Theorem rabbiia 3185

Description: Equivalent wff's yield equal restricted class abstractions (inference rule). (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
rabbiia.1	|- ( x e. A -> ( ph <-> ps ) )

Assertion

Ref	Expression
rabbiia	|- { x e. A | ph } = { x e. A | ps }

Proof of Theorem rabbiia

Step	Hyp	Ref	Expression
1		rabbiia.1	. . . 4 |- ( x e. A -> ( ph <-> ps ) )
2	1	pm5.32i 669	. . 3 |- ( ( x e. A /\ ph ) <-> ( x e. A /\ ps ) )
3	2	abbii 2739	. 2 |- { x | ( x e. A /\ ph ) } = { x | ( x e. A /\ ps ) }
4		df-rab 2921	. 2 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
5		df-rab 2921	. 2 |- { x e. A | ps } = { x | ( x e. A /\ ps ) }
6	3, 4, 5	3eqtr4i 2654	1 |- { x e. A | ph } = { x e. A | ps }

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   {cab 2608   {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-rab 2921

This theorem is referenced by:  elneldisj  3963  elnelun  3964  elneldisjOLD  3965  elnelunOLD  3966  dfepfr  5099  epfrc  5100  fndmdifcom  6322  fniniseg2  6340  fninfp  6440  fndifnfp  6442  bm2.5ii  7006  nlimon  7051  dfom2  7067  dfoi  8416  rankval2  8681  kmlem3  8974  alephsuc3  9402  ioopos  12250  hashbclem  13236  gcdcom  15235  gcdass  15264  lcmcom  15306  lcmass  15327  prmreclem4  15623  acsfn0  16321  acsfn1  16322  acsfn2  16324  dfrhm2  18717  lbsextg  19162  dmtopon  20727  fctop2  20809  ordtrest2  21008  qtopres  21501  tsmsfbas  21931  shftmbl  23306  logtayl  24406  ftalem3  24801  ppiub  24929  rpvmasum  25215  umgrislfupgrlem  26017  vtxdginducedm1  26439  finsumvtxdg2ssteplem1  26441  finsumvtxdg2size  26446  rgrusgrprc  26485  clwwlknclwwlkdifs  26873  numclwwlkovf2num  27218  ubthlem1  27726  fpwrelmapffslem  29507  xpinpreima  29952  xpinpreima2  29953  ordtrest2NEW  29969  unelldsys  30221  rossros  30243  aean  30307  eulerpartgbij  30434  orvcval2  30520  subfacp1lem6  31167  noextendlt  31822  nosepne  31831  nosepdm  31834  nosupbnd2lem1  31861  noetalem3  31865  topdifinfeq  33198  itg2addnclem2  33462  scottexf  33976  scott0f  33977  rabbii  34014  rabimbieq  34016  glbconxN  34664  3anrabdioph  37346  3orrabdioph  37347  rexrabdioph  37358  2rexfrabdioph  37360  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  elnn0rabdioph  37367  elnnrabdioph  37371  rabren3dioph  37379  rmydioph  37581  rmxdioph  37583  expdiophlem2  37589  expdioph  37590  relintab  37889  fsovrfovd  38303  k0004val0  38452  nzss  38516  hashnzfz  38519  uzmptshftfval  38545  binomcxplemdvsum  38554  binomcxp  38556  dvnprod  40164  fourierdlem90  40413  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem100  40423  fourierdlem109  40432  fourierdlem110  40433  fourierdlem112  40435  fourierdlem113  40436  ovnsubadd  40786  hoidmv1lelem3  40807  hoidmvlelem3  40811  ovolval3  40861  ovolval4lem2  40864  ovolval5lem3  40868  sssmf  40947  smflimlem4  40982  dfodd6  41550  dfeven4  41551  dfeven2  41562  dfodd3  41563  dfeven3  41570  dfodd4  41571  dfodd5  41572