Theorem abbii 2806

Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993.) Remove dependency on ax-10 2138, ax-11 2154, and ax-12 2174. (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 2804	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
2		abbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1793	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Syntax hints:   ↔ wb 206   = wceq 1536  {cab 2711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726

This theorem is referenced by:  rabbiiaOLD  3437  rabrab  3457  dfv2  3480  rabab  3509  csb2  3909  cbvcsbw  3917  cbvcsb  3918  cbvcsbv  3919  csbid  3920  csbcow  3922  csbco  3923  csbconstg  3926  csbie  3943  cbvreucsf  3954  unabw  4312  notabw  4318  unrab  4320  inrab  4321  inrab2  4322  difrab  4323  rabun2  4329  dfnul4  4340  dfnul2  4341  dfnul3  4342  abf  4411  dfif2  4532  dfsn2ALT  4651  rabsnifsb  4726  tprot  4753  pw0  4816  pwpw0  4817  dfopif  4874  pwsn  4904  dfuni2  4913  dfint2  4952  dfiunv2  5039  cbviun  5040  cbviin  5041  cbviung  5042  cbviing  5043  cbviunv  5044  cbviinv  5045  iunrab  5056  iunidOLD  5065  viin  5069  iunsn  5070  iinuni  5102  cbvopab  5219  cbvopabv  5220  cbvopab1  5222  cbvopab1g  5223  cbvopab2  5224  cbvopab1s  5225  cbvopab1v  5226  cbvopab2v  5228  unopab  5229  zfrep4  5298  zfpair  5426  iunopab  5568  iunopabOLD  5569  dfid2  5584  dfid3  5585  rabxp  5736  csbxp  5787  dfdm3  5900  dfrn2  5901  dfrn3  5902  dfdm4  5908  dfdmf  5909  csbdm  5910  dmun  5923  dmopab  5928  dmopabss  5931  dmopab3  5932  dfrnf  5963  rnopab  5967  rnopabss  5968  rnopab3  5969  rnmpt  5970  dfima2  6081  dfima3  6082  imadmrn  6089  imai  6093  args  6112  mptpreima  6259  dfiota2  6516  cbviotaw  6522  cbviotavw  6523  cbviota  6524  sb8iota  6526  mptfnf  6703  dffv4  6903  dfimafn2  6971  opabiotadm  6989  fndmin  7064  dffo3f  7125  fnasrn  7164  elabrex  7261  elabrexg  7262  abrexco  7263  dfoprab2  7490  cbvoprab2  7520  cbvoprab12v  7522  cbvoprab3v  7524  dmoprab  7534  rnoprab  7536  rnoprab2  7537  fnrnov  7605  abnex  7775  uniuni  7780  zfrep6  7977  fvresex  7982  abrexex2g  7987  abexssex  7993  abexex  7994  oprabrexex2  8001  dfopab2  8075  poseq  8181  soseq  8182  suppvalbr  8187  cnvimadfsn  8195  dfwrecsOLD  8336  dfrecs3  8410  dfrecs3OLD  8411  rdglem1  8453  snec  8818  pmex  8869  fset0  8892  f1setex  8895  0map0sn0  8923  dfixp  8937  cbvixp  8952  cbvixpv  8953  pwfir  9352  marypha2lem4  9475  tcsni  9780  scottexs  9924  scott0s  9925  kardex  9931  cardf2  9980  dfac3  10158  infmap2  10254  cf0  10288  cfval2  10297  isf33lem  10403  dffin1-5  10425  axdc2lem  10485  addcompr  11058  mulcompr  11060  dfnn3  12277  hashf1lem2  14491  prprrab  14508  cshwsexa  14858  cshwsexaOLD  14859  trclun  15049  shftdm  15106  hashbc0  17038  lubfval  18407  glbfval  18420  odulub  18464  oduglb  18466  symgbas0  19420  symgsubmefmnd  19430  pmtrprfvalrn  19520  efgval2  19756  dvdsrval  20377  dfrhm2  20490  toponsspwpw  22943  tgval2  22978  tgdif0  23014  xkobval  23609  ustfn  24225  ustn0  24244  2lgslem1b  27450  2sq  27488  madeval2  27906  addsasslem1  28050  addsasslem2  28051  negsid  28087  addsdilem1  28191  addsdilem2  28192  mulsasslem1  28203  mulsasslem2  28204  1p1e2s  28414  nohalf  28421  0reno  28443  rusgrprc  29622  rgrprcx  29624  wwlksnfi  29935  clwwlkvbij  30141  dfconngr1  30216  isconngr  30217  isconngr1  30218  nmopnegi  31993  nmop0  32014  nmfn0  32015  sa-abvi  32471  dmrab  32524  abrexdomjm  32534  abrexexd  32536  cbviunf  32575  dfimafnf  32652  ofpreima  32681  intimafv  32725  cnvoprabOLD  32737  maprnin  32748  fpwrelmapffslem  32749  hasheuni  34065  sigaex  34090  sigaval  34091  eulerpartlemt  34352  bnj1146  34783  bnj1400  34827  bnj882  34918  bnj893  34920  dfacycgr1  35128  derang0  35153  subfaclefac  35160  satfdm  35353  fmla0  35366  fmlasuc0  35368  fmla1  35371  dfon2lem7  35770  dfon2  35773  dfrdg2  35776  dfiota3  35904  fvline  36125  ellines  36133  sbceqbii  36172  rabeqbii  36175  iuneq12i  36176  iineq1i  36177  iineq12i  36178  ixpeq1i  36181  cbvcsbvw2  36213  cbviunvw2  36214  cbviinvw2  36215  cbvoprab1vw  36219  cbvoprab2vw  36220  cbvoprab123vw  36221  cbvoprab23vw  36222  cbvoprab13vw  36223  cbvixpvw2  36227  bj-df-ifc  36562  bj-dfif  36563  bj-rababw  36863  bj-inrab  36909  bj-taginv  36968  bj-nuliotaALT  37040  bj-dfid2ALT  37047  rnmptsn  37317  dissneqlem  37322  dissneq  37323  dffinxpf  37367  rabiun  37579  ismblfin  37647  volsupnfl  37651  areacirclem5  37698  abrexdom  37716  sdclem1  37729  sdc  37730  rncnvepres  38284  qsresid  38306  rnxrn  38379  rncossdmcoss  38436  dfcoeleqvrels  38602  mpets  38823  psubspset  39726  pmapglb  39752  polval2N  39888  psubclsetN  39918  tendoset  40741  sticksstones16  42143  sticksstones21  42148  imaopab  42248  prjspeclsp  42598  sn-isghm  42659  eq0rabdioph  42763  rexrabdioph  42781  eldioph4b  42798  hbtlem6  43117  onsucrn  43260  dfno2  43417  alephiso2  43547  dfid7  43601  clcnvlem  43612  dfrtrcl5  43618  relopabVD  44898  iuneq1i  45024  dfaiota2  47035  dfaimafn2  47115  fundcmpsurinj  47333  fundcmpsurbijinj  47334  sprid  47398  stgr1  47863  setrec2  48925