Theorem abbii 2836

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

Syntax hints:   ↔ wb 209   = wceq 1567  {cab 2747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761

This theorem is referenced by:  dfv2  3466  rabab  3493  csb2  3863  cbvcsbw  3871  cbvcsb  3872  cbvcsbv  3873  csbid  3874  csbcow  3876  csbco  3877  csbconstg  3880  csbie  3896  cbvreucsf  3905  unabw  4268  notabw  4274  unrab  4276  inrab  4277  inrab2  4278  difrab  4279  rabun2  4285  dfnul4  4296  dfnul2  4297  dfnul3  4298  abf  4377  dfif2  4494  dfsn2ALT  4616  rabsnifsb  4693  tprot  4720  pw0  4782  pwpw0  4783  dfopif  4839  pwsn  4869  dfuni2  4878  dfint2  4918  dfiunv2  5002  cbviun  5003  cbviin  5004  cbviung  5005  cbviing  5006  cbviunv  5007  cbviinv  5008  iunrab  5021  viin  5033  iunsn  5034  iinuni  5068  cbvopab  5187  cbvopabv  5188  cbvopab1  5189  cbvopab1g  5190  cbvopab2  5191  cbvopab1s  5192  cbvopab1v  5193  cbvopab2v  5194  unopab  5195  zfrep4  5258  zfpair  5393  iunopab  5545  dfid2  5559  dfid3  5560  rabxp  5710  csbxp  5763  dfdm3  5878  dfrn2  5879  dfrn3  5880  dfdm4  5886  dfdmf  5887  csbdm  5888  dmun  5901  dmopab  5906  dmopabss  5909  dmopab3  5910  dfrnf  5941  rnopab  5945  rnopabss  5946  rnopab3  5947  rnmpt  5948  dfima2  6065  dfima3  6066  imadmrn  6073  imai  6077  args  6095  mptpreima  6240  dfiota2  6494  cbviotaw  6500  cbviotavw  6501  cbviota  6502  sb8iota  6504  mptfnf  6671  dffv4  6879  dfimafn2  6945  opabiotadm  6963  fndmin  7041  dffo3f  7102  fnasrn  7142  elabrex  7241  elabrexg  7242  abrexco  7243  dfoprab2  7469  cbvoprab2  7499  cbvoprab12v  7501  cbvoprab3v  7503  dmoprab  7514  rnoprab  7516  rnoprab2  7517  fnrnov  7584  abnex  7755  uniuni  7760  zfrep6OLD  7951  fvresex  7956  abrexex2g  7960  abexssex  7966  abexex  7967  oprabrexex2  7974  dfopab2  8048  poseq  8153  soseq  8154  suppvalbr  8159  cnvimadfsn  8167  dfrecs3  8358  rdglem1  8401  snec  8775  pmex  8828  fset0  8850  f1setex  8853  0map0sn0  8882  dfixp  8896  cbvixp  8911  cbvixpv  8912  pwfir  9275  marypha2lem4  9397  tcsni  9709  scottexs  9860  scott0s  9861  kardex  9879  cardf2  9928  dfac3  10104  infmap2  10199  cf0  10233  cfval2  10243  isf33lem  10349  dffin1-5  10371  axdc2lem  10431  addcompr  11005  mulcompr  11007  dfnn3  12246  hashf1lem2  14492  prprrab  14509  cshwsexa  14860  trclun  15050  shftdm  15107  hashbc0  17064  lubfval  18403  glbfval  18416  odulub  18460  oduglb  18462  symgbas0  19458  symgsubmefmnd  19467  pmtrprfvalrn  19557  efgval2  19793  dvdsrval  20442  dfrhm2  20555  toponsspwpw  23047  tgval2  23081  tgdif0  23117  xkobval  23711  ustfn  24327  ustn0  24346  2lgslem1b  27521  2sq  27559  madeval2  27991  addsasslem1  28161  addsasslem2  28162  negsid  28199  addsdilem1  28309  addsdilem2  28310  mulsasslem1  28321  mulsasslem2  28322  twocut  28581  pw2cut2  28620  rusgrprc  29880  rgrprcx  29882  wwlksnfi  30195  clwwlkvbij  30404  dfconngr1  30479  isconngr  30480  isconngr1  30481  nmopnegi  32257  nmop0  32278  nmfn0  32279  sa-abvi  32735  dmrab  32783  abrexdomjm  32793  abrexexd  32795  cbviunf  32840  dfimafnf  32921  ofpreima  32950  intimafv  32996  maprnin  33016  fpwrelmapffslem  33017  hasheuni  34419  sigaex  34444  sigaval  34445  eulerpartlemt  34705  bnj1146  35123  bnj1400  35167  bnj882  35258  bnj893  35260  dfacycgr1  35534  derang0  35559  subfaclefac  35566  satfdm  35759  fmla0  35772  fmlasuc0  35774  fmla1  35777  dfon2lem7  36177  dfon2  36180  dfrdg2  36183  dfiota3  36311  fvline  36534  ellines  36542  sbceqbii  36591  rabeqbii  36594  iuneq12i  36595  iineq1i  36596  iineq12i  36597  ixpeq1i  36600  cbvcsbvw2  36631  cbviunvw2  36632  cbviinvw2  36633  cbvoprab1vw  36637  cbvoprab2vw  36638  cbvoprab123vw  36639  cbvoprab23vw  36640  cbvoprab13vw  36641  cbvixpvw2  36645  bj-dfnul2  37051  bj-df-ifc  37061  bj-dfif  37062  bj-rababw  37404  bj-inrab  37450  bj-taginv  37509  bj-nuliotaALT  37581  bj-dfid2ALT  37588  rnmptsn  37868  dissneqlem  37873  dissneq  37874  dffinxpf  37918  rabiun  38131  ismblfin  38199  volsupnfl  38203  areacirclem5  38250  abrexdom  38268  sdclem1  38281  sdc  38282  rncnvepres  38847  qsresid  38869  dmxrn  38925  dmcnvep  38926  rnxrn  38959  dfsuccl3  39011  dfsuccl4  39012  rncossdmcoss  39083  dfcoeleqvrels  39243  mpets  39494  psubspset  40407  pmapglb  40433  polval2N  40569  psubclsetN  40599  tendoset  41422  sticksstones16  42818  sticksstones21  42823  imaopab  42891  prjspeclsp  43235  sn-isghm  43296  eq0rabdioph  43398  rexrabdioph  43412  eldioph4b  43429  hbtlem6  43747  onsucrn  43889  dfno2  44045  alephiso2  44175  dfid7  44229  clcnvlem  44240  dfrtrcl5  44246  relopabVD  45500  iuneq1i  45695  dfaiota2  47711  dfaimafn2  47791  fundcmpsurinj  48046  fundcmpsurbijinj  48047  sprid  48111  stgr1  48614  setrec2  50357