Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  abbii Structured version   Visualization version   GIF version

Theorem abbii 2863
 Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993.) Remove dependency on ax-10 2142, ax-11 2158, and ax-12 2175. (Revised by Steven Nguyen, 3-May-2023.)
Hypothesis
Ref Expression
abbii.1 (𝜑𝜓)
Assertion
Ref Expression
abbii {𝑥𝜑} = {𝑥𝜓}

Proof of Theorem abbii
StepHypRef Expression
1 abbi1 2861 . 2 (∀𝑥(𝜑𝜓) → {𝑥𝜑} = {𝑥𝜓})
2 abbii.1 . 2 (𝜑𝜓)
31, 2mpg 1799 1 {𝑥𝜑} = {𝑥𝜓}
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   = wceq 1538  {cab 2776 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791 This theorem is referenced by:  rabrab  3332  rabbiia  3419  rabab  3470  csb2  3830  cbvcsbw  3838  cbvcsb  3839  csbid  3841  csbcow  3843  csbco  3844  cbvreucsf  3872  ss2abdv  3991  unrab  4226  inrab  4227  inrab2  4228  difrab  4229  rabun2  4234  dfnul2  4245  dfnul3  4246  abf  4310  dfif2  4427  dfsn2ALT  4545  rabsnifsb  4618  tprot  4645  pw0  4705  pwpw0  4706  dfopif  4760  pwsn  4792  pwsnOLD  4793  dfuni2  4802  unipr  4817  dfint2  4840  dfiunv2  4922  cbviun  4923  cbviin  4924  cbviung  4925  cbviing  4926  iunrab  4939  iunid  4947  viin  4951  iinuni  4983  cbvopab  5101  cbvopab1  5103  cbvopab1g  5104  cbvopab2  5105  cbvopab1s  5106  cbvopab2v  5108  unopab  5109  zfrep4  5164  zfpair  5287  iunopab  5411  dfid3  5427  rabxp  5564  csbxp  5614  dfdm3  5722  dfrn2  5723  dfrn3  5724  dfdm4  5728  dfdmf  5729  csbdm  5730  dmun  5743  dmopab  5748  dmopabss  5751  dmopab3  5752  domepOLD  5758  dfrnf  5784  rnopab  5790  rnmpt  5791  dfima2  5898  dfima3  5899  imadmrn  5906  imai  5909  args  5924  mptpreima  6059  dfiota2  6284  cbviotaw  6290  cbviota  6292  sb8iota  6294  mptfnf  6455  dffv4  6642  dfimafn2  6704  opabiotadm  6720  fndmin  6792  fnasrn  6884  elabrex  6980  abrexco  6981  dfoprab2  7191  cbvoprab2  7221  dmoprab  7234  rnoprab  7236  rnoprab2  7237  fnrnov  7302  abnex  7461  uniuni  7466  zfrep6  7640  fvresex  7645  abrexex2g  7649  abexssex  7655  abexex  7656  oprabrexex2  7663  dfopab2  7734  suppvalbr  7819  cnvimadfsn  7824  dfrecs3  7994  rdglem1  8036  snec  8345  pmex  8396  0map0sn0  8434  dfixp  8448  cbvixp  8463  marypha2lem4  8888  ruv  9052  tcsni  9171  scottexs  9302  scott0s  9303  kardex  9309  cardf2  9358  dfac3  9534  infmap2  9631  cf0  9664  cfval2  9673  isf33lem  9779  dffin1-5  9801  axdc2lem  9861  addcompr  10434  mulcompr  10436  dfnn3  11641  hashf1lem2  13812  prprrab  13829  cshwsexa  14179  trclun  14367  shftdm  14424  hashbc0  16333  lubfval  17582  glbfval  17595  oduglb  17743  odulub  17745  symgbas0  18512  symgsubmefmnd  18521  pmtrprfvalrn  18611  efgval2  18845  dvdsrval  19394  dfrhm2  19468  toponsspwpw  21534  tgval2  21568  tgdif0  21604  xkobval  22198  ustfn  22814  ustn0  22833  2lgslem1b  25983  2sq  26021  rusgrprc  27387  rgrprcx  27389  wwlksnfi  27699  clwwlkvbij  27905  dfconngr1  27980  isconngr  27981  isconngr1  27982  nmopnegi  29755  nmop0  29776  nmfn0  29777  sa-abvi  30233  dmrab  30274  abrexdomjm  30282  abrexexd  30284  cbviunf  30326  dfimafnf  30402  ofpreima  30435  intimafv  30477  cnvoprabOLD  30489  maprnin  30500  fpwrelmapffslem  30501  hasheuni  31466  sigaex  31491  sigaval  31492  eulerpartlemt  31751  bnj1146  32185  bnj1400  32229  bnj882  32320  bnj893  32322  dfacycgr1  32516  derang0  32541  subfaclefac  32548  satfdm  32741  fmla0  32754  fmlasuc0  32756  fmla1  32759  dfon2lem7  33159  dfon2  33162  dfrdg2  33165  poseq  33220  soseq  33221  madeval2  33415  dfiota3  33509  fvline  33730  ellines  33738  bj-df-ifc  34042  bj-dfif  34043  bj-rababw  34337  bj-inrab  34385  bj-taginv  34438  bj-nuliotaALT  34491  rnmptsn  34768  dissneqlem  34773  dissneq  34774  dffinxpf  34818  wl-dfrabsb  35042  rabiun  35046  ismblfin  35114  volsupnfl  35118  areacirclem5  35165  abrexdom  35184  sdclem1  35197  sdc  35198  rncnvepres  35737  qsresid  35758  rnxrn  35822  rncossdmcoss  35871  dfcoeleqvrels  36032  psubspset  37056  pmapglb  37082  polval2N  37218  psubclsetN  37248  tendoset  38071  iunsn  39428  imaopab  39429  prjspeclsp  39621  eq0rabdioph  39732  rexrabdioph  39750  eldioph4b  39767  hbtlem6  40088  alephiso2  40272  dfid7  40327  clcnvlem  40338  dfrtrcl5  40344  relopabVD  41622  elabrexg  41690  dffo3f  41821  dfaiota2  43658  dfaimafn2  43737  fundcmpsurinj  43941  fundcmpsurbijinj  43942  sprid  44006  setrec2  45239
 Copyright terms: Public domain W3C validator