Theorem abbii 2846

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

Syntax hints:   ↔ wb 198   = wceq 1508  {cab 2760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-9 2060  ax-ext 2752

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-sb 2017  df-clab 2761  df-cleq 2773

This theorem is referenced by:  rabrab  3320  rabswap  3325  rabbiia  3400  rabab  3446  csb2  3790  cbvcsb  3793  csbid  3796  csbco  3798  cbvreucsf  3824  unrab  4164  inrab  4165  inrab2  4166  difrab  4167  rabun2  4172  dfnul2  4183  dfnul3  4185  dfif2  4355  dfsn2ALT  4464  rabsnifsb  4537  tprot  4564  pw0  4624  pwpw0  4625  dfopif  4679  pwsn  4709  pwsnALT  4710  dfuni2  4719  unipr  4730  dfint2  4756  dfiunv2  4835  cbviun  4836  cbviin  4837  iunrab  4847  iunid  4855  viin  4859  iinuni  4891  cbvopab  5005  cbvopab1  5007  cbvopab2  5008  cbvopab1s  5009  cbvopab2v  5011  unopab  5012  zfrep4  5062  zfpair  5182  iunopab  5302  dfid3  5317  rabxp  5456  csbxp  5504  dfdm3  5612  dfrn2  5613  dfrn3  5614  dfdm4  5618  dfdmf  5619  csbdm  5620  dmun  5633  dmopab  5638  dmopabss  5639  dmopab3  5640  dfrnf  5668  rnopab  5674  rnmpt  5675  dfima2  5777  dfima3  5778  imadmrn  5785  imai  5787  args  5802  mptpreima  5936  dfiota2  6158  cbviota  6162  sb8iota  6164  mptfnf  6318  dffv4  6501  dfimafn2  6564  opabiotadm  6579  fndmin  6646  fnasrn  6736  elabrex  6833  abrexco  6834  dfoprab2  7037  cbvoprab2  7064  dmoprab  7077  rnoprab  7079  rnoprab2  7080  fnrnov  7143  abnex  7302  uniuni  7307  zfrep6  7474  fvresex  7479  abrexex2g  7483  abexssex  7489  abexex  7490  oprabrexex2  7497  dfopab2  7564  suppvalbr  7643  cnvimadfsn  7648  dfrecs3  7819  rdglem1  7861  snec  8166  pmex  8217  dfixp  8267  cbvixp  8282  marypha2lem4  8703  ruv  8867  tcsni  8985  scottexs  9116  scott0s  9117  kardex  9123  cardf2  9172  dfac3  9347  infmap2  9444  cf0  9477  cfval2  9486  isf33lem  9592  dffin1-5  9614  axdc2lem  9674  addcompr  10247  mulcompr  10249  dfnn3  11461  hashf1lem2  13633  prprrab  13648  cshwsexa  14054  trclun  14241  shftdm  14297  hashbc0  16203  lubfval  17458  glbfval  17471  oduglb  17619  odulub  17621  symgbas0  18295  pmtrprfvalrn  18389  efgval2  18620  dvdsrval  19130  dfrhm2  19204  toponsspwpw  21249  tgval2  21283  tgdif0  21319  xkobval  21913  ustfn  22528  ustn0  22547  2lgslem1b  25685  2sq  25723  rusgrprc  27090  rgrprcx  27092  wwlksnfi  27420  wwlksnfiOLD  27421  clwwlkvbij  27656  clwwlkvbijOLD  27657  dfconngr1  27732  isconngr  27733  isconngr1  27734  nmopnegi  29538  nmop0  29559  nmfn0  29560  sa-abvi  30016  dmrab  30054  abrexdomjm  30061  abrexexd  30063  cbviunf  30093  dfimafnf  30160  ofpreima  30189  cnvoprabOLD  30232  maprnin  30243  fpwrelmapffslem  30244  hasheuni  31020  sigaex  31045  sigaval  31046  isrnsigaOLD  31048  eulerpartlemt  31306  bnj1146  31743  bnj1400  31787  bnj882  31877  bnj893  31879  derang0  32041  subfaclefac  32048  fmla0  32232  fmlasuc0  32234  fmla1  32237  dfon2lem7  32594  dfon2  32597  domep  32598  dfrdg2  32601  poseq  32656  soseq  32657  madeval2  32851  dfiota3  32945  fvline  33166  ellines  33174  bj-dfifc2  33470  bj-df-ifc  33471  bj-rababw  33730  bj-inrab  33780  bj-taginv  33856  bj-nuliotaALT  33902  rnmptsn  34098  dissneqlem  34103  dissneq  34104  dffinxpf  34147  wl-dfrabsb  34342  rabiun  34346  ismblfin  34414  volsupnfl  34418  areacirclem5  34467  abrexdom  34487  sdclem1  34500  sdc  34501  rncnvepres  35045  qsresid  35066  rnxrn  35131  rncossdmcoss  35180  dfcoeleqvrels  35341  psubspset  36365  pmapglb  36391  polval2N  36527  psubclsetN  36557  tendoset  37380  iunsn  38604  imaopab  38605  prjspeclsp  38710  eq0rabdioph  38810  rexrabdioph  38828  eldioph4b  38845  hbtlem6  39166  dfid7  39376  clcnvlem  39387  dfrtrcl5  39393  relopabVD  40694  elabrexg  40762  dffo3f  40899  dfaiota2  42727  dfaimafn2  42806  sprid  43039  setrec2  44200