Theorem abbii 2886

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

Syntax hints:   ↔ wb 208   = wceq 1537  {cab 2799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814

This theorem is referenced by:  rabrab  3379  rabbiia  3472  rabab  3523  csb2  3885  cbvcsbw  3893  cbvcsb  3894  csbid  3896  csbcow  3898  csbco  3899  cbvreucsf  3927  unrab  4274  inrab  4275  inrab2  4276  difrab  4277  rabun2  4282  dfnul2  4293  dfnul3  4295  dfif2  4469  dfsn2ALT  4587  rabsnifsb  4658  tprot  4685  pw0  4745  pwpw0  4746  dfopif  4800  pwsn  4830  pwsnOLD  4831  dfuni2  4840  unipr  4855  dfint2  4878  dfiunv2  4960  cbviun  4961  cbviin  4962  cbviung  4963  cbviing  4964  iunrab  4976  iunid  4984  viin  4988  iinuni  5020  cbvopab  5137  cbvopab1  5139  cbvopab1g  5140  cbvopab2  5141  cbvopab1s  5142  cbvopab2v  5144  unopab  5145  zfrep4  5200  zfpair  5322  iunopab  5446  dfid3  5462  rabxp  5600  csbxp  5650  dfdm3  5758  dfrn2  5759  dfrn3  5760  dfdm4  5764  dfdmf  5765  csbdm  5766  dmun  5779  dmopab  5784  dmopabss  5787  dmopab3  5788  domepOLD  5794  dfrnf  5820  rnopab  5826  rnmpt  5827  dfima2  5931  dfima3  5932  imadmrn  5939  imai  5942  args  5957  mptpreima  6092  dfiota2  6315  cbviotaw  6321  cbviota  6323  sb8iota  6325  mptfnf  6483  dffv4  6667  dfimafn2  6729  opabiotadm  6745  fndmin  6815  fnasrn  6907  elabrex  7002  abrexco  7003  dfoprab2  7212  cbvoprab2  7242  dmoprab  7255  rnoprab  7257  rnoprab2  7258  fnrnov  7321  abnex  7479  uniuni  7484  zfrep6  7656  fvresex  7661  abrexex2g  7665  abexssex  7671  abexex  7672  oprabrexex2  7679  dfopab2  7750  suppvalbr  7834  cnvimadfsn  7839  dfrecs3  8009  rdglem1  8051  snec  8360  pmex  8411  0map0sn0  8449  dfixp  8463  cbvixp  8478  marypha2lem4  8902  ruv  9066  tcsni  9185  scottexs  9316  scott0s  9317  kardex  9323  cardf2  9372  dfac3  9547  infmap2  9640  cf0  9673  cfval2  9682  isf33lem  9788  dffin1-5  9810  axdc2lem  9870  addcompr  10443  mulcompr  10445  dfnn3  11652  hashf1lem2  13815  prprrab  13832  cshwsexa  14186  trclun  14374  shftdm  14430  hashbc0  16341  lubfval  17588  glbfval  17601  oduglb  17749  odulub  17751  symgbas0  18517  symgsubmefmnd  18526  pmtrprfvalrn  18616  efgval2  18850  dvdsrval  19395  dfrhm2  19469  toponsspwpw  21530  tgval2  21564  tgdif0  21600  xkobval  22194  ustfn  22810  ustn0  22829  2lgslem1b  25968  2sq  26006  rusgrprc  27372  rgrprcx  27374  wwlksnfi  27684  wwlksnfiOLD  27685  clwwlkvbij  27892  dfconngr1  27967  isconngr  27968  isconngr1  27969  nmopnegi  29742  nmop0  29763  nmfn0  29764  sa-abvi  30220  dmrab  30260  abrexdomjm  30267  abrexexd  30269  cbviunf  30307  dfimafnf  30381  ofpreima  30410  cnvoprabOLD  30456  maprnin  30467  fpwrelmapffslem  30468  hasheuni  31344  sigaex  31369  sigaval  31370  eulerpartlemt  31629  bnj1146  32063  bnj1400  32107  bnj882  32198  bnj893  32200  dfacycgr1  32391  derang0  32416  subfaclefac  32423  satfdm  32616  fmla0  32629  fmlasuc0  32631  fmla1  32634  dfon2lem7  33034  dfon2  33037  dfrdg2  33040  poseq  33095  soseq  33096  madeval2  33290  dfiota3  33384  fvline  33605  ellines  33613  bj-df-ifc  33913  bj-dfif  33914  bj-rababw  34200  bj-inrab  34248  bj-taginv  34301  bj-nuliotaALT  34354  rnmptsn  34619  dissneqlem  34624  dissneq  34625  dffinxpf  34669  wl-dfrabsb  34876  rabiun  34880  ismblfin  34948  volsupnfl  34952  areacirclem5  35001  abrexdom  35020  sdclem1  35033  sdc  35034  rncnvepres  35576  qsresid  35597  rnxrn  35661  rncossdmcoss  35710  dfcoeleqvrels  35871  psubspset  36895  pmapglb  36921  polval2N  37057  psubclsetN  37087  tendoset  37910  iunsn  39167  imaopab  39168  prjspeclsp  39311  eq0rabdioph  39422  rexrabdioph  39440  eldioph4b  39457  hbtlem6  39778  alephiso2  39966  dfid7  40021  clcnvlem  40032  dfrtrcl5  40038  relopabVD  41284  elabrexg  41352  dffo3f  41487  dfaiota2  43335  dfaimafn2  43414  fundcmpsurinj  43618  fundcmpsurbijinj  43619  sprid  43685  setrec2  44847