Theorem abbii 2832

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  {cab 2743

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757

This theorem is used by:  dfv2  3460  rabab  3487  csb2  3856  cbvcsbw  3864  cbvcsb  3865  cbvcsbv  3866  csbid  3867  csbcow  3869  csbco  3870  csbconstg  3873  csbie  3889  cbvreucsf  3898  unabw  4260  notabw  4266  unrab  4268  inrab  4269  inrab2  4270  difrab  4271  rabun2  4277  dfnul4  4288  dfnul2  4289  dfnul3  4290  abf  4371  dfif2  4491  dfsn2ALT  4613  rabsnifsb  4690  tprot  4717  pw0  4780  pwpw0  4781  dfopif  4837  pwsn  4867  dfuni2  4876  dfint2  4916  dfiunv2  5000  cbviun  5001  cbviin  5002  cbviung  5003  cbviing  5004  cbviunv  5005  cbviinv  5006  iunrab  5019  viin  5031  iunsn  5032  iinuni  5066  cbvopab  5185  cbvopabv  5186  cbvopab1  5187  cbvopab1g  5188  cbvopab2  5189  cbvopab1s  5190  cbvopab1v  5191  cbvopab2v  5192  unopab  5193  zfrep4  5256  zfpair  5394  iunopab  5546  dfid2  5560  dfid3  5561  rabxp  5711  csbxp  5764  dfdm3  5879  dfrn2  5880  dfrn3  5881  dfdm4  5887  dfdmf  5888  csbdm  5889  dmun  5902  dmopab  5907  dmopabss  5910  dmopab3  5911  dfrnf  5942  rnopab  5946  rnopabss  5947  rnopab3  5948  rnmpt  5949  dfima2  6066  dfima3  6067  imadmrn  6074  imai  6078  args  6096  mptpreima  6241  dfiota2  6497  cbviotaw  6503  cbviotavw  6504  cbviota  6505  sb8iota  6507  mptfnf  6674  dffv4  6882  dfimafn2  6948  opabiotadm  6966  fndmin  7044  dffo3f  7105  fnasrn  7147  elabrex  7245  elabrexg  7246  abrexco  7247  dfoprab2  7477  cbvoprab2  7507  cbvoprab12v  7509  cbvoprab3v  7511  dmoprab  7522  rnoprab  7524  rnoprab2  7525  fnrnov  7593  abnex  7762  uniuni  7767  zfrep6OLD  7958  fvresex  7963  abrexex2g  7967  abexssex  7973  abexex  7974  oprabrexex2  7981  dfopab2  8055  poseq  8160  soseq  8161  suppvalbr  8166  cnvimadfsn  8174  dfrecs3  8365  rdglem1  8408  snec  8782  pmex  8835  fset0  8857  f1setex  8860  0map0sn0  8889  dfixp  8903  cbvixp  8918  cbvixpv  8919  pwfir  9283  marypha2lem4  9405  tcsni  9717  scottexsOLD  9879  scott0bsOLD  9881  kardexOLD  9894  cardf2  9945  dfac3  10121  infmap2  10216  cf0  10249  cfval2  10259  isf33lem  10365  dffin1-5  10387  axdc2lem  10447  addcompr  11021  mulcompr  11023  dfnn3  12262  hashf1lem2  14511  prprrab  14528  cshwsexa  14885  trclun  15075  shftdm  15132  hashbc0  17087  lubfval  18426  glbfval  18439  odulub  18483  oduglb  18485  symgbas0  19503  symgsubmefmnd  19512  pmtrprfvalrn  19602  efgval2  19838  dvdsrval  20489  dfrhm2  20602  toponsspwpw  23129  tgval2  23163  tgdif0  23199  xkobval  23794  ustfn  24410  ustn0  24429  2lgslem1b  27607  2sq  27645  madeval2  28077  addsasslem1  28247  addsasslem2  28248  negsid  28285  addsdilem1  28395  addsdilem2  28396  mulsasslem1  28407  mulsasslem2  28408  twocut  28667  pw2cut2  28706  rusgrprc  29998  rgrprcx  30000  wwlksnfi  30322  clwwlkvbij  30531  dfconngr1  30610  isconngr  30611  isconngr1  30612  nmopnegi  32388  nmop0  32409  nmfn0  32410  sa-abvi  32866  dmrab  32914  abrexdomjm  32924  abrexexd  32926  cbviunf  32971  dfimafnf  33052  ofpreima  33081  intimafv  33127  maprnin  33146  fpwrelmapffslem  33147  hasheuni  34539  sigaex  34564  sigaval  34565  eulerpartlemt  34826  bnj1146  35244  bnj1400  35288  bnj882  35379  bnj893  35381  dfacycgr1  35673  derang0  35698  subfaclefac  35705  satfdm  35898  fmla0  35911  fmlasuc0  35913  fmla1  35916  dfon2lem7  36316  dfon2  36319  dfrdg2  36322  dfiota3  36450  fvline  36673  ellines  36681  sbceqbii  36760  rabeqbii  36763  iuneq12i  36764  iineq1i  36765  iineq12i  36766  ixpeq1i  36769  cbvcsbvw2  36800  cbviunvw2  36801  cbviinvw2  36802  cbvoprab1vw  36806  cbvoprab2vw  36807  cbvoprab123vw  36808  cbvoprab23vw  36809  cbvoprab13vw  36810  cbvixpvw2  36814  bj-dfnul2  37220  bj-df-ifc  37230  bj-dfif  37231  bj-rababw  37573  bj-inrab  37620  bj-taginv  37679  bj-nuliotaALT  37751  bj-dfid2ALT  37758  rnmptsn  38038  dissneqlem  38043  dissneq  38044  dffinxpf  38088  rabiun  38301  ismblfin  38369  volsupnfl  38373  areacirclem5  38420  abrexdom  38439  sdclem1  38452  sdc  38453  rncnvepres  39016  qsresid  39038  dmxrn  39094  dmcnvep  39095  rnxrn  39128  dfsuccl3  39180  dfsuccl4  39181  rncossdmcoss  39252  dfcoeleqvrels  39412  mpets  39663  psubspset  40576  pmapglb  40602  polval2N  40738  psubclsetN  40768  tendoset  41591  sticksstones16  42987  sticksstones21  42992  imaopab  43060  prjspeclsp  43402  sn-isghm  43463  eq0rabdioph  43565  rexrabdioph  43579  eldioph4b  43596  hbtlem6  43914  onsucrn  44056  dfno2  44212  alephiso2  44342  dfid7  44396  clcnvlem  44407  dfrtrcl5  44413  relopabVD  45667  iuneq1i  45862  dfaiota2  47881  dfaimafn2  47961  fundcmpsurinj  48216  fundcmpsurbijinj  48217  sprid  48281  stgr1  48784  setrec2  50530