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

Theorem abbii 2768
Description: Equivalent wff's yield equal class abstractions (inference rule). (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
abbii.1 (𝜑𝜓)
Assertion
Ref Expression
abbii {𝑥𝜑} = {𝑥𝜓}

Proof of Theorem abbii
StepHypRef Expression
1 abbi 2766 . 2 (∀𝑥(𝜑𝜓) ↔ {𝑥𝜑} = {𝑥𝜓})
2 abbii.1 . 2 (𝜑𝜓)
31, 2mpgbi 1765 1 {𝑥𝜑} = {𝑥𝜓}
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523  {cab 2637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647
This theorem is referenced by:  rabrab  3146  rabswap  3151  rabbiia  3215  rabab  3254  csb2  3568  cbvcsb  3571  csbid  3574  csbco  3576  cbvreucsf  3600  unrab  3931  inrab  3932  inrab2  3933  difrab  3934  rabun2  3939  dfnul3  3951  rab0OLD  3989  dfif2  4121  rabsnifsb  4289  tprot  4316  pw0  4375  pwpw0  4376  dfopif  4430  pwsn  4460  pwsnALT  4461  dfuni2  4470  unipr  4481  dfint2  4509  int0OLD  4523  dfiunv2  4588  cbviun  4589  cbviin  4590  iunrab  4599  iunid  4607  viin  4611  iinuni  4641  cbvopab  4754  cbvopab1  4756  cbvopab2  4757  cbvopab1s  4758  cbvopab2v  4760  unopab  4761  zfrep4  4812  zfpair  4934  iunopab  5041  dfid3  5054  rabxp  5188  csbxp  5234  dfdm3  5342  dfrn2  5343  dfrn3  5344  dfdm4  5348  dfdmf  5349  csbdm  5350  dmun  5363  dmopab  5367  dmopabss  5368  dmopab3  5369  dfrnf  5396  rnopab  5402  rnmpt  5403  dfima2  5503  dfima3  5504  imadmrn  5511  imai  5513  args  5528  mptpreima  5666  dfiota2  5890  cbviota  5894  sb8iota  5896  mptfnf  6053  dffv4  6226  dfimafn2  6285  opabiotadm  6299  fndmin  6364  fnasrn  6451  elabrex  6541  abrexco  6542  dfoprab2  6743  cbvoprab2  6770  dmoprab  6783  rnoprab  6785  rnoprab2  6786  fnrnov  6849  abnex  7007  uniuni  7013  zfrep6  7176  fvresex  7181  abrexex2g  7186  abexssex  7191  abrexex2OLD  7192  abexex  7193  oprabrexex2  7200  dfopab2  7266  suppvalbr  7344  cnvimadfsn  7349  dfrecs3  7514  rdglem1  7556  snec  7853  pmex  7904  dfixp  7952  cbvixp  7967  marypha2lem4  8385  ruv  8545  tcsni  8657  scottexs  8788  scott0s  8789  kardex  8795  cardf2  8807  dfac3  8982  infmap2  9078  cf0  9111  cfval2  9120  isf33lem  9226  dffin1-5  9248  axdc2lem  9308  addcompr  9881  mulcompr  9883  dfnn3  11072  hashf1lem2  13278  prprrab  13293  cshwsexa  13616  trclun  13799  shftdm  13855  hashbc0  15756  lubfval  17025  glbfval  17038  oduglb  17186  odulub  17188  symgbas0  17860  pmtrprfvalrn  17954  efgval2  18183  dvdsrval  18691  dfrhm2  18765  toponsspwpw  20774  tgval2  20808  tgdif0  20844  xkobval  21437  ustfn  22052  ustn0  22071  2lgslem1b  25162  2sq  25200  rusgrprc  26542  rgrprcx  26544  wwlksnfi  26869  wlksnwwlknvbij  26871  clwwlkvbij  27088  clwwlkvbijOLD  27089  dfconngr1  27166  isconngr  27167  isconngr1  27168  nmopnegi  28952  nmop0  28973  nmfn0  28974  foo3  29430  abrexdomjm  29471  abrexexd  29473  cbviunf  29498  dfimafnf  29564  ofpreima  29593  cnvoprabOLD  29626  maprnin  29634  fpwrelmapffslem  29635  hasheuni  30275  sigaex  30300  sigaval  30301  isrnsigaOLD  30303  eulerpartlemt  30561  ballotlem2  30678  bnj1146  30988  bnj1400  31032  bnj882  31122  bnj893  31124  derang0  31277  subfaclefac  31284  dfon2lem7  31818  dfon2  31821  domep  31822  dfrdg2  31825  poseq  31878  soseq  31879  madeval2  32061  dfiota3  32155  fvline  32376  ellines  32384  bj-dfifc2  32689  bj-df-ifc  32690  bj-inrab  33048  bj-taginv  33099  bj-nuliotaALT  33145  rnmptsn  33312  dissneqlem  33317  dissneq  33318  dffinxpf  33352  rabiun  33512  ismblfin  33580  volsupnfl  33584  areacirclem5  33634  abrexdom  33655  sdclem1  33669  sdc  33670  rncnvepres  34214  qsresid  34237  rnxrn  34296  rncossdmcoss  34345  psubspset  35348  pmapglb  35374  polval2N  35510  psubclsetN  35540  tendoset  36364  eq0rabdioph  37657  rexrabdioph  37675  eldioph4b  37692  hbtlem6  38016  dfid7  38236  clcnvlem  38247  dfrtrcl5  38253  relopabVD  39451  elabrexg  39520  dffo3f  39678  dfaimafn2  41567  sprid  42049  setrec2  42767
  Copyright terms: Public domain W3C validator