Theorem abbii 2806

Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993.) Remove dependency on ax-10 2152, ax-11 2168, and ax-12 2189. (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 1804	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Syntax hints:   ↔ wb 207   = wceq 1547  {cab 2717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731

This theorem is referenced by:  dfv2  3434  rabab  3461  csb2  3833  cbvcsbw  3841  cbvcsb  3842  cbvcsbv  3843  csbid  3844  csbcow  3846  csbco  3847  csbconstg  3850  csbie  3866  cbvreucsf  3875  unabw  4235  notabw  4241  unrab  4243  inrab  4244  inrab2  4245  difrab  4246  rabun2  4252  dfnul4  4263  dfnul2  4264  dfnul3  4265  abf  4334  dfif2  4456  dfsn2ALT  4577  rabsnifsb  4654  tprot  4681  pw0  4743  pwpw0  4744  dfopif  4801  pwsn  4831  dfuni2  4840  dfint2  4879  dfiunv2  4963  cbviun  4964  cbviin  4965  cbviung  4966  cbviing  4967  cbviunv  4968  cbviinv  4969  iunrab  4982  viin  4994  iunsn  4995  iinuni  5027  cbvopab  5144  cbvopabv  5145  cbvopab1  5146  cbvopab1g  5147  cbvopab2  5148  cbvopab1s  5149  cbvopab1v  5150  cbvopab2v  5151  unopab  5152  zfrep4  5215  zfpair  5350  iunopab  5501  dfid2  5515  dfid3  5516  rabxp  5666  csbxp  5719  dfdm3  5829  dfrn2  5830  dfrn3  5831  dfdm4  5837  dfdmf  5838  csbdm  5839  dmun  5852  dmopab  5857  dmopabss  5860  dmopab3  5861  dfrnf  5892  rnopab  5896  rnopabss  5897  rnopab3  5898  rnmpt  5899  dfima2  6014  dfima3  6015  imadmrn  6022  imai  6026  args  6044  mptpreima  6189  dfiota2  6442  cbviotaw  6448  cbviotavw  6449  cbviota  6450  sb8iota  6452  mptfnf  6620  dffv4  6824  dfimafn2  6890  opabiotadm  6908  fndmin  6986  dffo3f  7047  fnasrn  7087  elabrex  7186  elabrexg  7187  abrexco  7188  dfoprab2  7414  cbvoprab2  7444  cbvoprab12v  7446  cbvoprab3v  7448  dmoprab  7459  rnoprab  7461  rnoprab2  7462  fnrnov  7529  abnex  7700  uniuni  7705  zfrep6OLD  7897  fvresex  7902  abrexex2g  7906  abexssex  7912  abexex  7913  oprabrexex2  7920  dfopab2  7994  poseq  8098  soseq  8099  suppvalbr  8104  cnvimadfsn  8112  dfrecs3  8302  rdglem1  8344  snec  8715  pmex  8768  fset0  8791  f1setex  8794  0map0sn0  8823  dfixp  8837  cbvixp  8852  cbvixpv  8853  pwfir  9217  marypha2lem4  9341  tcsni  9653  scottexs  9802  scott0s  9803  kardex  9809  cardf2  9858  dfac3  10034  infmap2  10130  cf0  10164  cfval2  10173  isf33lem  10279  dffin1-5  10301  axdc2lem  10361  addcompr  10935  mulcompr  10937  dfnn3  12179  hashf1lem2  14409  prprrab  14426  cshwsexa  14777  trclun  14967  shftdm  15024  hashbc0  16967  lubfval  18305  glbfval  18318  odulub  18362  oduglb  18364  symgbas0  19355  symgsubmefmnd  19364  pmtrprfvalrn  19454  efgval2  19690  dvdsrval  20332  dfrhm2  20445  toponsspwpw  22905  tgval2  22939  tgdif0  22975  xkobval  23569  ustfn  24185  ustn0  24204  2lgslem1b  27373  2sq  27411  madeval2  27843  addsasslem1  28013  addsasslem2  28014  negsid  28051  addsdilem1  28161  addsdilem2  28162  mulsasslem1  28173  mulsasslem2  28174  twocut  28433  pw2cut2  28472  rusgrprc  29677  rgrprcx  29679  wwlksnfi  29992  clwwlkvbij  30201  dfconngr1  30276  isconngr  30277  isconngr1  30278  nmopnegi  32054  nmop0  32075  nmfn0  32076  sa-abvi  32532  dmrab  32584  abrexdomjm  32595  abrexexd  32597  cbviunf  32644  dfimafnf  32728  ofpreima  32757  intimafv  32803  maprnin  32823  fpwrelmapffslem  32824  hasheuni  34269  sigaex  34294  sigaval  34295  eulerpartlemt  34555  bnj1146  34973  bnj1400  35017  bnj882  35108  bnj893  35110  dfacycgr1  35372  derang0  35397  subfaclefac  35404  satfdm  35597  fmla0  35610  fmlasuc0  35612  fmla1  35615  dfon2lem7  36015  dfon2  36018  dfrdg2  36021  dfiota3  36149  fvline  36372  ellines  36380  sbceqbii  36419  rabeqbii  36422  iuneq12i  36423  iineq1i  36424  iineq12i  36425  ixpeq1i  36428  cbvcsbvw2  36459  cbviunvw2  36460  cbviinvw2  36461  cbvoprab1vw  36465  cbvoprab2vw  36466  cbvoprab123vw  36467  cbvoprab23vw  36468  cbvoprab13vw  36469  cbvixpvw2  36473  bj-dfnul2  36881  bj-df-ifc  36891  bj-dfif  36892  bj-rababw  37234  bj-inrab  37280  bj-taginv  37339  bj-nuliotaALT  37411  bj-dfid2ALT  37418  rnmptsn  37697  dissneqlem  37702  dissneq  37703  dffinxpf  37747  rabiun  37960  ismblfin  38028  volsupnfl  38032  areacirclem5  38079  abrexdom  38097  sdclem1  38110  sdc  38111  rncnvepres  38676  qsresid  38698  dmxrn  38754  dmcnvep  38755  rnxrn  38788  dfsuccl3  38840  dfsuccl4  38841  rncossdmcoss  38912  dfcoeleqvrels  39072  mpets  39323  psubspset  40236  pmapglb  40262  polval2N  40398  psubclsetN  40428  tendoset  41251  sticksstones16  42647  sticksstones21  42652  imaopab  42718  prjspeclsp  43062  sn-isghm  43123  eq0rabdioph  43225  rexrabdioph  43239  eldioph4b  43256  hbtlem6  43574  onsucrn  43716  dfno2  43872  alephiso2  44002  dfid7  44056  clcnvlem  44067  dfrtrcl5  44073  relopabVD  45344  iuneq1i  45532  dfaiota2  47549  dfaimafn2  47629  fundcmpsurinj  47884  fundcmpsurbijinj  47885  sprid  47949  stgr1  48452  setrec2  50185