Theorem abbii 2888

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 2886	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
2		abbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1798	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

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

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 2795

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

This theorem is referenced by:  rabrab  3381  rabbiia  3474  rabab  3525  csb2  3887  cbvcsbw  3895  cbvcsb  3896  csbid  3898  csbcow  3900  csbco  3901  cbvreucsf  3929  unrab  4276  inrab  4277  inrab2  4278  difrab  4279  rabun2  4284  dfnul2  4295  dfnul3  4297  dfif2  4471  dfsn2ALT  4589  rabsnifsb  4660  tprot  4687  pw0  4747  pwpw0  4748  dfopif  4802  pwsn  4832  pwsnOLD  4833  dfuni2  4842  unipr  4857  dfint2  4880  dfiunv2  4962  cbviun  4963  cbviin  4964  cbviung  4965  cbviing  4966  iunrab  4978  iunid  4986  viin  4990  iinuni  5022  cbvopab  5139  cbvopab1  5141  cbvopab1g  5142  cbvopab2  5143  cbvopab1s  5144  cbvopab2v  5146  unopab  5147  zfrep4  5202  zfpair  5324  iunopab  5448  dfid3  5464  rabxp  5602  csbxp  5652  dfdm3  5760  dfrn2  5761  dfrn3  5762  dfdm4  5766  dfdmf  5767  csbdm  5768  dmun  5781  dmopab  5786  dmopabss  5789  dmopab3  5790  domepOLD  5796  dfrnf  5822  rnopab  5828  rnmpt  5829  dfima2  5933  dfima3  5934  imadmrn  5941  imai  5944  args  5959  mptpreima  6094  dfiota2  6317  cbviotaw  6323  cbviota  6325  sb8iota  6327  mptfnf  6485  dffv4  6669  dfimafn2  6731  opabiotadm  6747  fndmin  6817  fnasrn  6909  elabrex  7004  abrexco  7005  dfoprab2  7214  cbvoprab2  7244  dmoprab  7257  rnoprab  7259  rnoprab2  7260  fnrnov  7323  abnex  7481  uniuni  7486  zfrep6  7658  fvresex  7663  abrexex2g  7667  abexssex  7673  abexex  7674  oprabrexex2  7681  dfopab2  7752  suppvalbr  7836  cnvimadfsn  7841  dfrecs3  8011  rdglem1  8053  snec  8362  pmex  8413  0map0sn0  8451  dfixp  8465  cbvixp  8480  marypha2lem4  8904  ruv  9068  tcsni  9187  scottexs  9318  scott0s  9319  kardex  9325  cardf2  9374  dfac3  9549  infmap2  9642  cf0  9675  cfval2  9684  isf33lem  9790  dffin1-5  9812  axdc2lem  9872  addcompr  10445  mulcompr  10447  dfnn3  11654  hashf1lem2  13817  prprrab  13834  cshwsexa  14188  trclun  14376  shftdm  14432  hashbc0  16343  lubfval  17590  glbfval  17603  oduglb  17751  odulub  17753  symgbas0  18519  symgsubmefmnd  18528  pmtrprfvalrn  18618  efgval2  18852  dvdsrval  19397  dfrhm2  19471  toponsspwpw  21532  tgval2  21566  tgdif0  21602  xkobval  22196  ustfn  22812  ustn0  22831  2lgslem1b  25970  2sq  26008  rusgrprc  27374  rgrprcx  27376  wwlksnfi  27686  wwlksnfiOLD  27687  clwwlkvbij  27894  dfconngr1  27969  isconngr  27970  isconngr1  27971  nmopnegi  29744  nmop0  29765  nmfn0  29766  sa-abvi  30222  dmrab  30262  abrexdomjm  30269  abrexexd  30271  cbviunf  30309  dfimafnf  30383  ofpreima  30412  cnvoprabOLD  30458  maprnin  30469  fpwrelmapffslem  30470  hasheuni  31346  sigaex  31371  sigaval  31372  eulerpartlemt  31631  bnj1146  32065  bnj1400  32109  bnj882  32200  bnj893  32202  dfacycgr1  32393  derang0  32418  subfaclefac  32425  satfdm  32618  fmla0  32631  fmlasuc0  32633  fmla1  32636  dfon2lem7  33036  dfon2  33039  dfrdg2  33042  poseq  33097  soseq  33098  madeval2  33292  dfiota3  33386  fvline  33607  ellines  33615  bj-df-ifc  33915  bj-dfif  33916  bj-rababw  34199  bj-inrab  34247  bj-taginv  34300  bj-nuliotaALT  34353  rnmptsn  34618  dissneqlem  34623  dissneq  34624  dffinxpf  34668  wl-dfrabsb  34863  rabiun  34867  ismblfin  34935  volsupnfl  34939  areacirclem5  34988  abrexdom  35007  sdclem1  35020  sdc  35021  rncnvepres  35563  qsresid  35584  rnxrn  35648  rncossdmcoss  35697  dfcoeleqvrels  35858  psubspset  36882  pmapglb  36908  polval2N  37044  psubclsetN  37074  tendoset  37897  iunsn  39125  imaopab  39126  prjspeclsp  39269  eq0rabdioph  39380  rexrabdioph  39398  eldioph4b  39415  hbtlem6  39736  alephiso2  39924  dfid7  39979  clcnvlem  39990  dfrtrcl5  39996  relopabVD  41242  elabrexg  41310  dffo3f  41445  dfaiota2  43293  dfaimafn2  43372  fundcmpsurinj  43576  fundcmpsurbijinj  43577  sprid  43643  setrec2  44805