Theorem abbii 2812

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

Syntax hints:   ↔ wb 206   = wceq 1537  {cab 2717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732

This theorem is referenced by:  rabbiiaOLD  3448  rabrab  3468  dfv2  3491  rabab  3520  csb2  3923  cbvcsbw  3931  cbvcsb  3932  cbvcsbv  3933  csbid  3934  csbcow  3936  csbco  3937  csbconstg  3940  csbie  3957  cbvreucsf  3968  unabw  4326  notabw  4332  unrab  4334  inrab  4335  inrab2  4336  difrab  4337  rabun2  4343  dfnul4  4354  dfnul2  4355  dfnul3  4356  dfnul2OLD  4357  dfnul3OLD  4358  dfnul4OLD  4359  abf  4429  dfif2  4550  dfsn2ALT  4669  rabsnifsb  4747  tprot  4774  pw0  4837  pwpw0  4838  dfopif  4894  pwsn  4924  dfuni2  4933  dfint2  4972  dfiunv2  5058  cbviun  5059  cbviin  5060  cbviung  5061  cbviing  5062  cbviunv  5063  cbviinv  5064  iunrab  5075  iunidOLD  5084  viin  5088  iunsn  5089  iinuni  5121  cbvopab  5238  cbvopabv  5239  cbvopab1  5241  cbvopab1g  5242  cbvopab2  5243  cbvopab1s  5244  cbvopab1v  5245  cbvopab2v  5247  unopab  5248  zfrep4  5314  zfpair  5439  iunopab  5578  iunopabOLD  5579  dfid2  5595  dfid3  5596  rabxp  5748  csbxp  5799  dfdm3  5912  dfrn2  5913  dfrn3  5914  dfdm4  5920  dfdmf  5921  csbdm  5922  dmun  5935  dmopab  5940  dmopabss  5943  dmopab3  5944  dfrnf  5975  rnopab  5979  rnmpt  5980  dfima2  6091  dfima3  6092  imadmrn  6099  imai  6103  args  6122  mptpreima  6269  dfiota2  6526  cbviotaw  6532  cbviotavw  6533  cbviota  6535  sb8iota  6537  mptfnf  6715  dffv4  6917  dfimafn2  6985  opabiotadm  7003  fndmin  7078  dffo3f  7140  fnasrn  7179  elabrex  7279  elabrexg  7280  abrexco  7281  dfoprab2  7508  cbvoprab2  7538  cbvoprab12v  7540  cbvoprab3v  7542  dmoprab  7552  rnoprab  7554  rnoprab2  7555  fnrnov  7623  abnex  7792  uniuni  7797  zfrep6  7995  fvresex  8000  abrexex2g  8005  abexssex  8011  abexex  8012  oprabrexex2  8019  dfopab2  8093  poseq  8199  soseq  8200  suppvalbr  8205  cnvimadfsn  8213  dfwrecsOLD  8354  dfrecs3  8428  dfrecs3OLD  8429  rdglem1  8471  snec  8838  pmex  8889  fset0  8912  f1setex  8915  0map0sn0  8943  dfixp  8957  cbvixp  8972  cbvixpv  8973  pwfir  9383  marypha2lem4  9507  tcsni  9812  scottexs  9956  scott0s  9957  kardex  9963  cardf2  10012  dfac3  10190  infmap2  10286  cf0  10320  cfval2  10329  isf33lem  10435  dffin1-5  10457  axdc2lem  10517  addcompr  11090  mulcompr  11092  dfnn3  12307  hashf1lem2  14505  prprrab  14522  cshwsexa  14872  cshwsexaOLD  14873  trclun  15063  shftdm  15120  hashbc0  17052  lubfval  18420  glbfval  18433  odulub  18477  oduglb  18479  symgbas0  19430  symgsubmefmnd  19440  pmtrprfvalrn  19530  efgval2  19766  dvdsrval  20387  dfrhm2  20500  toponsspwpw  22949  tgval2  22984  tgdif0  23020  xkobval  23615  ustfn  24231  ustn0  24250  2lgslem1b  27454  2sq  27492  madeval2  27910  addsasslem1  28054  addsasslem2  28055  negsid  28091  addsdilem1  28195  addsdilem2  28196  mulsasslem1  28207  mulsasslem2  28208  1p1e2s  28418  nohalf  28425  0reno  28447  rusgrprc  29626  rgrprcx  29628  wwlksnfi  29939  clwwlkvbij  30145  dfconngr1  30220  isconngr  30221  isconngr1  30222  nmopnegi  31997  nmop0  32018  nmfn0  32019  sa-abvi  32475  dmrab  32525  abrexdomjm  32535  abrexexd  32537  cbviunf  32578  dfimafnf  32655  ofpreima  32683  intimafv  32722  cnvoprabOLD  32734  maprnin  32745  fpwrelmapffslem  32746  hasheuni  34049  sigaex  34074  sigaval  34075  eulerpartlemt  34336  bnj1146  34767  bnj1400  34811  bnj882  34902  bnj893  34904  dfacycgr1  35112  derang0  35137  subfaclefac  35144  satfdm  35337  fmla0  35350  fmlasuc0  35352  fmla1  35355  dfon2lem7  35753  dfon2  35756  dfrdg2  35759  dfiota3  35887  fvline  36108  ellines  36116  sbceqbii  36155  rabeqbii  36158  iuneq12i  36159  iineq1i  36160  iineq12i  36161  ixpeq1i  36164  cbvcsbvw2  36197  cbviunvw2  36198  cbviinvw2  36199  cbvoprab1vw  36203  cbvoprab2vw  36204  cbvoprab123vw  36205  cbvoprab23vw  36206  cbvoprab13vw  36207  cbvixpvw2  36211  bj-df-ifc  36546  bj-dfif  36547  bj-rababw  36847  bj-inrab  36893  bj-taginv  36952  bj-nuliotaALT  37024  bj-dfid2ALT  37031  rnmptsn  37301  dissneqlem  37306  dissneq  37307  dffinxpf  37351  rabiun  37553  ismblfin  37621  volsupnfl  37625  areacirclem5  37672  abrexdom  37690  sdclem1  37703  sdc  37704  rncnvepres  38259  qsresid  38281  rnxrn  38354  rncossdmcoss  38411  dfcoeleqvrels  38577  mpets  38798  psubspset  39701  pmapglb  39727  polval2N  39863  psubclsetN  39893  tendoset  40716  sticksstones16  42119  sticksstones21  42124  imaopab  42224  prjspeclsp  42567  sn-isghm  42628  eq0rabdioph  42732  rexrabdioph  42750  eldioph4b  42767  hbtlem6  43086  onsucrn  43233  dfno2  43390  alephiso2  43520  dfid7  43574  clcnvlem  43585  dfrtrcl5  43591  relopabVD  44872  iuneq1i  44987  dfaiota2  47001  dfaimafn2  47081  fundcmpsurinj  47283  fundcmpsurbijinj  47284  sprid  47348  setrec2  48787