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

Theorem abbii 2395
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 2393 . 2  |-  ( A. x ( ph  <->  ps )  <->  { x  |  ph }  =  { x  |  ps } )
2 abbii.1 . 2  |-  ( ph  <->  ps )
31, 2mpgbi 1536 1  |-  { x  |  ph }  =  {
x  |  ps }
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623   {cab 2269
This theorem is referenced by:  rabswap  2719  rabbiia  2778  rabab  2805  csb2  3083  cbvcsb  3085  csbid  3088  csbco  3090  cbvreucsf  3145  unrab  3439  inrab  3440  inrab2  3441  difrab  3442  rabun2  3447  dfnul3  3458  rab0  3475  dfif2  3567  tprot  3722  pw0  3762  pwpw0  3763  dfopif  3793  pwsn  3821  pwsnALT  3822  dfuni2  3829  unipr  3841  dfint2  3864  int0  3876  cbviun  3939  cbviin  3940  iunrab  3949  iunid  3957  viin  3961  iinuni  3985  cbvopab  4087  cbvopab1  4089  cbvopab2  4090  cbvopab1s  4091  cbvopab2v  4093  unopab  4095  zfrep4  4139  zfpair  4212  iunopab  4296  dfid3  4310  uniuni  4527  rabxp  4725  dfdm3  4867  dfrn2  4868  dfrn3  4869  dfdm4  4872  dfdmf  4873  dmun  4885  dmopab  4889  dmopabss  4890  dmopab3  4891  dfrnf  4917  rnopab  4924  rnmpt  4925  dfima2  5014  dfima3  5015  imadmrn  5024  imai  5027  args  5041  mptpreima  5166  dfiota2  5220  cbviota  5224  sb8iota  5226  dffv4  5522  dfimafn2  5572  fndmin  5632  fnasrn  5702  zfrep6  5748  fvresex  5762  elabrex  5765  abrexco  5766  abrexex2g  5768  abrexex2  5780  abexssex  5781  abexex  5782  dfoprab2  5895  cbvoprab2  5919  dmoprab  5928  rnoprab  5930  rnoprab2  5931  oprabrexex2  5963  fnrnov  5993  dfopab2  6174  opabiotadm  6292  rdglem1  6428  snec  6722  pmex  6777  dfixp  6819  cbvixp  6833  marypha2lem4  7191  ruv  7314  tcsni  7428  scottexs  7557  scott0s  7558  kardex  7564  cardf2  7576  dfac3  7748  infmap2  7844  cf0  7877  cfval2  7886  isf33lem  7992  dffin1-5  8014  axdc2lem  8074  addcompr  8645  mulcompr  8647  dfnn3  9760  hashf1lem2  11394  shftdm  11566  cbvsum  12168  hashbc0  13052  efgval2  15033  dvdsrval  15427  dfrhm2  15498  tgval2  16694  tgdif0  16730  xkobval  17281  2sq  20615  nmopnegi  22545  nmop0  22566  nmfn0  22567  foo3  23023  dfimafnf  23041  ballotlem2  23047  abrexdomjm  23165  abrexexd  23192  mptfnf  23226  hasheuni  23453  sigaex  23470  sigaval  23471  isrnsigaOLD  23473  derang0  23700  subfaclefac  23707  vdgrun  23893  dfon2lem7  24145  dfon2  24148  domep  24149  dfrdg2  24152  poseq  24253  soseq  24254  tfrALTlem  24276  dfiota3  24462  fvline  24767  ellines  24775  areacirclem6  24930  clsbldimp  25088  isoriso  25212  dfps2  25289  dfdir2  25291  prodex  25304  cbvprodi  25312  imtr  25398  sallnei  25529  intopcoaconb  25540  isalg  25721  algi  25727  prismorcsetlem  25912  prismorcset  25914  dfiunv2  25916  iscola2  26092  abrexdom  26405  sdclem1  26453  sdc  26454  eq0rabdioph  26856  rexrabdioph  26875  eldioph4b  26894  hbtlem6  27333  dfaimafn2  28028  relopabVD  28677  bnj1146  28823  bnj1400  28868  bnj882  28958  bnj893  28960  psubspset  29933  pmapglb  29959  polval2N  30095  psubclsetN  30125  tendoset  30948
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276
  Copyright terms: Public domain W3C validator