Theorem abbii 2726

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

Hypothesis

Ref	Expression
abbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
abbii	⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Proof of Theorem abbii

Step	Hyp	Ref	Expression
1		abbi 2724	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
2		abbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpgbi 1716	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Syntax hints:   ↔ wb 195   = wceq 1475  {cab 2596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606

This theorem is referenced by:  rabswap  3098  rabbiia  3161  rabab  3196  csb2  3501  cbvcsb  3504  csbid  3507  csbco  3509  cbvreucsf  3533  unrab  3857  inrab  3858  inrab2  3859  difrab  3860  rabun2  3865  dfnul3  3877  rab0OLD  3910  dfif2  4038  rabsnifsb  4201  tprot  4228  pw0  4283  pwpw0  4284  dfopif  4337  pwsn  4366  pwsnALT  4367  dfuni2  4374  unipr  4385  dfint2  4412  int0OLD  4426  rabasiun  4459  dfiunv2  4492  cbviun  4493  cbviin  4494  iunrab  4503  iunid  4511  viin  4515  iinuni  4545  cbvopab  4653  cbvopab1  4655  cbvopab2  4656  cbvopab1s  4657  cbvopab2v  4659  unopab  4660  zfrep4  4707  zfpair  4831  iunopab  4936  dfid3  4954  rabxp  5078  csbxp  5123  dfdm3  5232  dfrn2  5233  dfrn3  5234  dfdm4  5238  dfdmf  5239  csbdm  5240  dmun  5253  dmopab  5257  dmopabss  5258  dmopab3  5259  dfrnf  5285  rnopab  5291  rnmpt  5292  dfima2  5387  dfima3  5388  imadmrn  5395  imai  5397  args  5412  mptpreima  5545  dfiota2  5769  cbviota  5773  sb8iota  5775  mptfnf  5928  dffv4  6100  dfimafn2  6156  opabiotadm  6170  fndmin  6232  fnasrn  6317  elabrex  6405  abrexco  6406  dfoprab2  6599  cbvoprab2  6626  dmoprab  6639  rnoprab  6641  rnoprab2  6642  fnrnov  6705  uniuni  6865  zfrep6  7027  fvresex  7032  abrexex2g  7036  abrexex2  7040  abexssex  7041  abexex  7042  oprabrexex2  7049  dfopab2  7113  suppvalbr  7186  cnvimadfsn  7191  dfrecs3  7356  rdglem1  7398  snec  7697  pmex  7749  dfixp  7796  cbvixp  7811  marypha2lem4  8227  ruv  8390  tcsni  8502  scottexs  8633  scott0s  8634  kardex  8640  cardf2  8652  dfac3  8827  infmap2  8923  cf0  8956  cfval2  8965  isf33lem  9071  dffin1-5  9093  axdc2lem  9153  addcompr  9722  mulcompr  9724  dfnn3  10911  hashf1lem2  13097  prprrab  13112  cshwsexa  13421  trclun  13603  shftdm  13659  hashbc0  15547  lubfval  16801  glbfval  16814  oduglb  16962  odulub  16964  symgbas0  17637  pmtrprfvalrn  17731  efgval2  17960  dvdsrval  18468  dfrhm2  18540  tgval2  20571  tgdif0  20607  xkobval  21199  ustfn  21815  ustn0  21834  2lgslem1b  24917  2sq  24955  usgraop  25879  wwlknprop  26214  wwlknfi  26266  wlknwwlknvbij  26268  clwwlkvbij  26329  vdgrun  26428  vdgrfiun  26429  nmopnegi  28208  nmop0  28229  nmfn0  28230  foo3  28686  rabrab  28722  abrexdomjm  28729  abrexexd  28731  cbviunf  28755  dfimafnf  28817  ofpreima  28848  cnvoprab  28886  maprnin  28894  fpwrelmapffslem  28895  hasheuni  29474  sigaex  29499  sigaval  29500  isrnsigaOLD  29502  eulerpartlemt  29760  ballotlem2  29877  bnj1146  30116  bnj1400  30160  bnj882  30250  bnj893  30252  derang0  30405  subfaclefac  30412  dfon2lem7  30938  dfon2  30941  domep  30942  dfrdg2  30945  poseq  30994  soseq  30995  dfiota3  31200  fvline  31421  ellines  31429  bj-dfifc2  31734  bj-df-ifc  31735  bj-inrab  32115  bj-taginv  32167  bj-nuliotaALT  32211  bj-toponss  32241  rnmptsn  32358  dissneqlem  32363  dissneq  32364  dffinxpf  32398  rabiun  32552  ismblfin  32620  volsupnfl  32624  areacirclem5  32674  abrexdom  32695  sdclem1  32709  sdc  32710  psubspset  34048  pmapglb  34074  polval2N  34210  psubclsetN  34240  tendoset  35065  eq0rabdioph  36358  rexrabdioph  36376  eldioph4b  36393  hbtlem6  36718  dfid7  36938  clcnvlem  36949  dfrtrcl5  36955  relopabVD  38159  elabrexg  38229  dffo3f  38359  dfaimafn2  39895  rusgrprc  40790  rgrprcx  40792  wwlksnfi  41112  wlksnwwlknvbij  41114  clwwlksvbij  41229  dfconngr1  41355  isconngr  41356  isconngr1  41357  setrec2  42241