Theorem abbii 2739

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

Hypothesis

Ref	Expression
abbii.1	|- ( ph <-> ps )

Assertion

Ref	Expression
abbii	|- { x | ph } = { x | ps }

Proof of Theorem abbii

Step	Hyp	Ref	Expression
1		abbi 2737	. 2 |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
2		abbii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpgbi 1725	1 |- { x | ph } = { x | ps }

Syntax hints:   <-> wb 196   = wceq 1483   {cab 2608

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

This theorem is referenced by:  rabswap  3121  rabbiia  3185  rabab  3223  csb2  3535  cbvcsb  3538  csbid  3541  csbco  3543  cbvreucsf  3567  unrab  3898  inrab  3899  inrab2  3900  difrab  3901  rabun2  3906  dfnul3  3918  rab0OLD  3956  dfif2  4088  rabsnifsb  4257  tprot  4284  pw0  4343  pwpw0  4344  dfopif  4399  pwsn  4428  pwsnALT  4429  dfuni2  4438  unipr  4449  dfint2  4477  int0OLD  4491  dfiunv2  4556  cbviun  4557  cbviin  4558  iunrab  4567  iunid  4575  viin  4579  iinuni  4609  cbvopab  4721  cbvopab1  4723  cbvopab2  4724  cbvopab1s  4725  cbvopab2v  4727  unopab  4728  zfrep4  4779  zfpair  4904  iunopab  5012  dfid3  5025  rabxp  5154  csbxp  5200  dfdm3  5310  dfrn2  5311  dfrn3  5312  dfdm4  5316  dfdmf  5317  csbdm  5318  dmun  5331  dmopab  5335  dmopabss  5336  dmopab3  5337  dfrnf  5364  rnopab  5370  rnmpt  5371  dfima2  5468  dfima3  5469  imadmrn  5476  imai  5478  args  5493  mptpreima  5628  dfiota2  5852  cbviota  5856  sb8iota  5858  mptfnf  6015  dffv4  6188  dfimafn2  6246  opabiotadm  6260  fndmin  6324  fnasrn  6411  elabrex  6501  abrexco  6502  dfoprab2  6701  cbvoprab2  6728  dmoprab  6741  rnoprab  6743  rnoprab2  6744  fnrnov  6807  abnex  6965  uniuni  6971  zfrep6  7134  fvresex  7139  abrexex2g  7144  abexssex  7149  abrexex2OLD  7150  abexex  7151  oprabrexex2  7158  dfopab2  7222  suppvalbr  7299  cnvimadfsn  7304  dfrecs3  7469  rdglem1  7511  snec  7810  pmex  7862  dfixp  7910  cbvixp  7925  marypha2lem4  8344  ruv  8507  tcsni  8619  scottexs  8750  scott0s  8751  kardex  8757  cardf2  8769  dfac3  8944  infmap2  9040  cf0  9073  cfval2  9082  isf33lem  9188  dffin1-5  9210  axdc2lem  9270  addcompr  9843  mulcompr  9845  dfnn3  11034  hashf1lem2  13240  prprrab  13255  cshwsexa  13570  trclun  13755  shftdm  13811  hashbc0  15709  lubfval  16978  glbfval  16991  oduglb  17139  odulub  17141  symgbas0  17814  pmtrprfvalrn  17908  efgval2  18137  dvdsrval  18645  dfrhm2  18717  toponsspwpw  20726  tgval2  20760  tgdif0  20796  xkobval  21389  ustfn  22005  ustn0  22024  2lgslem1b  25117  2sq  25155  rusgrprc  26486  rgrprcx  26488  wwlksnfi  26801  wlksnwwlknvbij  26803  clwwlksvbij  26922  dfconngr1  27048  isconngr  27049  isconngr1  27050  nmopnegi  28824  nmop0  28845  nmfn0  28846  foo3  29302  rabrab  29338  abrexdomjm  29345  abrexexd  29347  cbviunf  29372  dfimafnf  29436  ofpreima  29465  cnvoprab  29498  maprnin  29506  fpwrelmapffslem  29507  hasheuni  30147  sigaex  30172  sigaval  30173  isrnsigaOLD  30175  eulerpartlemt  30433  ballotlem2  30550  bnj1146  30862  bnj1400  30906  bnj882  30996  bnj893  30998  derang0  31151  subfaclefac  31158  dfon2lem7  31694  dfon2  31697  domep  31698  dfrdg2  31701  poseq  31750  soseq  31751  madeval2  31936  dfiota3  32030  fvline  32251  ellines  32259  bj-dfifc2  32564  bj-df-ifc  32565  bj-inrab  32923  bj-taginv  32974  bj-nuliotaALT  33020  rnmptsn  33182  dissneqlem  33187  dissneq  33188  dffinxpf  33222  rabiun  33382  ismblfin  33450  volsupnfl  33454  areacirclem5  33504  abrexdom  33525  sdclem1  33539  sdc  33540  rncnvepres  34073  qsresid  34096  psubspset  35030  pmapglb  35056  polval2N  35192  psubclsetN  35222  tendoset  36047  eq0rabdioph  37340  rexrabdioph  37358  eldioph4b  37375  hbtlem6  37699  dfid7  37919  clcnvlem  37930  dfrtrcl5  37936  relopabVD  39137  elabrexg  39206  dffo3f  39364  dfaimafn2  41246  sprid  41724  setrec2  42442