Theorem abbii 2796

Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993.) Remove dependency on ax-10 2142, ax-11 2158, and ax-12 2178. (Revised by Steven Nguyen, 3-May-2023.)

Hypothesis

Ref	Expression
abbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

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

Proof of Theorem abbii

Step	Hyp	Ref	Expression
1		abbi 2794	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
2		abbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1797	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Syntax hints:   ↔ wb 206   = wceq 1540  {cab 2707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721

This theorem is referenced by:  rabbiiaOLD  3407  rabrab  3427  dfv2  3447  rabab  3475  csb2  3861  cbvcsbw  3869  cbvcsb  3870  cbvcsbv  3871  csbid  3872  csbcow  3874  csbco  3875  csbconstg  3878  csbie  3894  cbvreucsf  3903  unabw  4266  notabw  4272  unrab  4274  inrab  4275  inrab2  4276  difrab  4277  rabun2  4283  dfnul4  4294  dfnul2  4295  dfnul3  4296  abf  4365  dfif2  4486  dfsn2ALT  4607  rabsnifsb  4682  tprot  4709  pw0  4772  pwpw0  4773  dfopif  4830  pwsn  4860  dfuni2  4869  dfint2  4908  dfiunv2  4994  cbviun  4995  cbviin  4996  cbviung  4997  cbviing  4998  cbviunv  4999  cbviinv  5000  iunrab  5011  iunidOLD  5020  viin  5024  iunsn  5025  iinuni  5057  cbvopab  5174  cbvopabv  5175  cbvopab1  5176  cbvopab1g  5177  cbvopab2  5178  cbvopab1s  5179  cbvopab1v  5180  cbvopab2v  5181  unopab  5182  zfrep4  5243  zfpair  5371  iunopab  5514  dfid2  5528  dfid3  5529  rabxp  5679  csbxp  5730  dfdm3  5841  dfrn2  5842  dfrn3  5843  dfdm4  5849  dfdmf  5850  csbdm  5851  dmun  5864  dmopab  5869  dmopabss  5872  dmopab3  5873  dfrnf  5903  rnopab  5907  rnopabss  5908  rnopab3  5909  rnmpt  5910  dfima2  6022  dfima3  6023  imadmrn  6030  imai  6034  args  6052  mptpreima  6199  dfiota2  6453  cbviotaw  6459  cbviotavw  6460  cbviota  6461  sb8iota  6463  mptfnf  6635  dffv4  6837  dfimafn2  6906  opabiotadm  6924  fndmin  6999  dffo3f  7060  fnasrn  7099  elabrex  7198  elabrexg  7199  abrexco  7200  dfoprab2  7427  cbvoprab2  7457  cbvoprab12v  7459  cbvoprab3v  7461  dmoprab  7472  rnoprab  7474  rnoprab2  7475  fnrnov  7542  abnex  7713  uniuni  7718  zfrep6  7913  fvresex  7918  abrexex2g  7922  abexssex  7928  abexex  7929  oprabrexex2  7936  dfopab2  8010  poseq  8114  soseq  8115  suppvalbr  8120  cnvimadfsn  8128  dfrecs3  8318  rdglem1  8360  snec  8728  pmex  8781  fset0  8804  f1setex  8807  0map0sn0  8835  dfixp  8849  cbvixp  8864  cbvixpv  8865  pwfir  9242  marypha2lem4  9365  tcsni  9672  scottexs  9816  scott0s  9817  kardex  9823  cardf2  9872  dfac3  10050  infmap2  10146  cf0  10180  cfval2  10189  isf33lem  10295  dffin1-5  10317  axdc2lem  10377  addcompr  10950  mulcompr  10952  dfnn3  12176  hashf1lem2  14397  prprrab  14414  cshwsexa  14765  cshwsexaOLD  14766  trclun  14956  shftdm  15013  hashbc0  16952  lubfval  18285  glbfval  18298  odulub  18342  oduglb  18344  symgbas0  19295  symgsubmefmnd  19304  pmtrprfvalrn  19394  efgval2  19630  dvdsrval  20246  dfrhm2  20359  toponsspwpw  22785  tgval2  22819  tgdif0  22855  xkobval  23449  ustfn  24065  ustn0  24084  2lgslem1b  27279  2sq  27317  madeval2  27737  addsasslem1  27886  addsasslem2  27887  negsid  27923  addsdilem1  28030  addsdilem2  28031  mulsasslem1  28042  mulsasslem2  28043  1p1e2s  28278  twocut  28285  0reno  28324  rusgrprc  29494  rgrprcx  29496  wwlksnfi  29809  clwwlkvbij  30015  dfconngr1  30090  isconngr  30091  isconngr1  30092  nmopnegi  31867  nmop0  31888  nmfn0  31889  sa-abvi  32345  dmrab  32399  abrexdomjm  32409  abrexexd  32411  cbviunf  32457  dfimafnf  32533  ofpreima  32562  intimafv  32607  maprnin  32627  fpwrelmapffslem  32628  hasheuni  34048  sigaex  34073  sigaval  34074  eulerpartlemt  34335  bnj1146  34754  bnj1400  34798  bnj882  34889  bnj893  34891  dfacycgr1  35104  derang0  35129  subfaclefac  35136  satfdm  35329  fmla0  35342  fmlasuc0  35344  fmla1  35347  dfon2lem7  35750  dfon2  35753  dfrdg2  35756  dfiota3  35884  fvline  36105  ellines  36113  sbceqbii  36152  rabeqbii  36155  iuneq12i  36156  iineq1i  36157  iineq12i  36158  ixpeq1i  36161  cbvcsbvw2  36192  cbviunvw2  36193  cbviinvw2  36194  cbvoprab1vw  36198  cbvoprab2vw  36199  cbvoprab123vw  36200  cbvoprab23vw  36201  cbvoprab13vw  36202  cbvixpvw2  36206  bj-df-ifc  36541  bj-dfif  36542  bj-rababw  36842  bj-inrab  36888  bj-taginv  36947  bj-nuliotaALT  37019  bj-dfid2ALT  37026  rnmptsn  37296  dissneqlem  37301  dissneq  37302  dffinxpf  37346  rabiun  37560  ismblfin  37628  volsupnfl  37632  areacirclem5  37679  abrexdom  37697  sdclem1  37710  sdc  37711  rncnvepres  38264  qsresid  38286  dmxrn  38333  dmcnvep  38334  rnxrn  38357  rncossdmcoss  38419  dfcoeleqvrels  38585  mpets  38807  psubspset  39711  pmapglb  39737  polval2N  39873  psubclsetN  39903  tendoset  40726  sticksstones16  42123  sticksstones21  42128  imaopab  42192  prjspeclsp  42573  sn-isghm  42634  eq0rabdioph  42737  rexrabdioph  42755  eldioph4b  42772  hbtlem6  43091  onsucrn  43233  dfno2  43390  alephiso2  43520  dfid7  43574  clcnvlem  43585  dfrtrcl5  43591  relopabVD  44863  iuneq1i  45052  dfaiota2  47060  dfaimafn2  47140  fundcmpsurinj  47383  fundcmpsurbijinj  47384  sprid  47448  stgr1  47933  setrec2  49657