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

Theorem abbii 2548
Description: Equivalent wff's yield equal class abstractions (inference rule). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
abbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
abbii  |-  { x  |  ph }  =  {
x  |  ps }

Proof of Theorem abbii
StepHypRef Expression
1 abbi 2546 . 2  |-  ( A. x ( ph  <->  ps )  <->  { x  |  ph }  =  { x  |  ps } )
2 abbii.1 . 2  |-  ( ph  <->  ps )
31, 2mpgbi 1558 1  |-  { x  |  ph }  =  {
x  |  ps }
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1652   {cab 2422
This theorem is referenced by:  rabswap  2887  rabbiia  2946  rabab  2973  csb2  3253  cbvcsb  3255  csbid  3258  csbco  3260  cbvreucsf  3313  unrab  3612  inrab  3613  inrab2  3614  difrab  3615  rabun2  3620  dfnul3  3631  rab0  3648  dfif2  3741  tprot  3899  pw0  3945  pwpw0  3946  dfopif  3981  pwsn  4009  pwsnALT  4010  dfuni2  4017  unipr  4029  dfint2  4052  int0  4064  dfiunv2  4127  cbviun  4128  cbviin  4129  iunrab  4138  iunid  4146  viin  4150  iinuni  4174  cbvopab  4276  cbvopab1  4278  cbvopab2  4279  cbvopab1s  4280  cbvopab2v  4282  unopab  4284  zfrep4  4328  zfpair  4401  iunopab  4486  dfid3  4499  uniuni  4716  rabxp  4914  dfdm3  5058  dfrn2  5059  dfrn3  5060  dfdm4  5063  dfdmf  5064  dmun  5076  dmopab  5080  dmopabss  5081  dmopab3  5082  dfrnf  5108  rnopab  5115  rnmpt  5116  dfima2  5205  dfima3  5206  imadmrn  5215  imai  5218  args  5232  mptpreima  5363  dfiota2  5419  cbviota  5423  sb8iota  5425  dffv4  5725  dfimafn2  5776  fndmin  5837  fnasrn  5912  zfrep6  5968  fvresex  5982  elabrex  5985  abrexco  5986  abrexex2g  5988  abrexex2  6001  abexssex  6002  abexex  6003  dfoprab2  6121  cbvoprab2  6145  dmoprab  6154  rnoprab  6156  rnoprab2  6157  oprabrexex2  6189  fnrnov  6219  dfopab2  6401  opabiotadm  6537  rdglem1  6673  snec  6967  pmex  7023  dfixp  7065  cbvixp  7079  marypha2lem4  7443  ruv  7568  tcsni  7682  scottexs  7811  scott0s  7812  kardex  7818  cardf2  7830  dfac3  8002  infmap2  8098  cf0  8131  cfval2  8140  isf33lem  8246  dffin1-5  8268  axdc2lem  8328  addcompr  8898  mulcompr  8900  dfnn3  10014  hashf1lem2  11705  shftdm  11886  hashbc0  13373  efgval2  15356  dvdsrval  15750  dfrhm2  15821  tgval2  17021  tgdif0  17057  xkobval  17618  ustfn  18231  ustn0  18250  2sq  21160  vdgrun  21672  vdgrfiun  21673  nmopnegi  23468  nmop0  23489  nmfn0  23490  foo3  23946  abrexdomjm  23988  abrexexd  23990  dfimafnf  24043  mptfnf  24073  ofpreima  24081  hasheuni  24475  sigaex  24492  sigaval  24493  isrnsigaOLD  24495  ballotlem2  24746  derang0  24855  subfaclefac  24862  dfon2lem7  25416  dfon2  25419  domep  25420  dfrdg2  25423  poseq  25528  soseq  25529  dfiota3  25768  fvline  26078  ellines  26086  rabiun  26236  ismblfin  26247  volsupnfl  26251  areacirclem5  26296  abrexdom  26432  sdclem1  26447  sdc  26448  eq0rabdioph  26835  rexrabdioph  26854  eldioph4b  26872  hbtlem6  27310  dfaimafn2  28006  cshwsexa  28291  relopabVD  29013  bnj1146  29162  bnj1400  29207  bnj882  29297  bnj893  29299  psubspset  30541  pmapglb  30567  polval2N  30703  psubclsetN  30733  tendoset  31556
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429
  Copyright terms: Public domain W3C validator