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

Theorem abbii 2408
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 2406 . 2  |-  ( A. x ( ph  <->  ps )  <->  { x  |  ph }  =  { x  |  ps } )
2 abbii.1 . 2  |-  ( ph  <->  ps )
31, 2mpgbi 1539 1  |-  { x  |  ph }  =  {
x  |  ps }
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1632   {cab 2282
This theorem is referenced by:  rabswap  2732  rabbiia  2791  rabab  2818  csb2  3096  cbvcsb  3098  csbid  3101  csbco  3103  cbvreucsf  3158  unrab  3452  inrab  3453  inrab2  3454  difrab  3455  rabun2  3460  dfnul3  3471  rab0  3488  dfif2  3580  tprot  3735  pw0  3778  pwpw0  3779  dfopif  3809  pwsn  3837  pwsnALT  3838  dfuni2  3845  unipr  3857  dfint2  3880  int0  3892  cbviun  3955  cbviin  3956  iunrab  3965  iunid  3973  viin  3977  iinuni  4001  cbvopab  4103  cbvopab1  4105  cbvopab2  4106  cbvopab1s  4107  cbvopab2v  4109  unopab  4111  zfrep4  4155  zfpair  4228  iunopab  4312  dfid3  4326  uniuni  4543  rabxp  4741  dfdm3  4883  dfrn2  4884  dfrn3  4885  dfdm4  4888  dfdmf  4889  dmun  4901  dmopab  4905  dmopabss  4906  dmopab3  4907  dfrnf  4933  rnopab  4940  rnmpt  4941  dfima2  5030  dfima3  5031  imadmrn  5040  imai  5043  args  5057  mptpreima  5182  dfiota2  5236  cbviota  5240  sb8iota  5242  dffv4  5538  dfimafn2  5588  fndmin  5648  fnasrn  5718  zfrep6  5764  fvresex  5778  elabrex  5781  abrexco  5782  abrexex2g  5784  abrexex2  5796  abexssex  5797  abexex  5798  dfoprab2  5911  cbvoprab2  5935  dmoprab  5944  rnoprab  5946  rnoprab2  5947  oprabrexex2  5979  fnrnov  6009  dfopab2  6190  opabiotadm  6308  rdglem1  6444  snec  6738  pmex  6793  dfixp  6835  cbvixp  6849  marypha2lem4  7207  ruv  7330  tcsni  7444  scottexs  7573  scott0s  7574  kardex  7580  cardf2  7592  dfac3  7764  infmap2  7860  cf0  7893  cfval2  7902  isf33lem  8008  dffin1-5  8030  axdc2lem  8090  addcompr  8661  mulcompr  8663  dfnn3  9776  hashf1lem2  11410  shftdm  11582  cbvsum  12184  hashbc0  13068  efgval2  15049  dvdsrval  15443  dfrhm2  15514  tgval2  16710  tgdif0  16746  xkobval  17297  2sq  20631  nmopnegi  22561  nmop0  22582  nmfn0  22583  foo3  23039  dfimafnf  23057  ballotlem2  23063  abrexdomjm  23181  abrexexd  23207  mptfnf  23241  hasheuni  23468  sigaex  23485  sigaval  23486  isrnsigaOLD  23488  derang0  23715  subfaclefac  23722  vdgrun  23908  dfon2lem7  24216  dfon2  24219  domep  24220  dfrdg2  24223  poseq  24324  soseq  24325  tfrALTlem  24347  dfiota3  24533  fvline  24839  ellines  24847  rabiun2  24997  areacirclem6  25033  clsbldimp  25191  isoriso  25315  dfps2  25392  dfdir2  25394  prodex  25407  cbvprodi  25415  imtr  25501  sallnei  25632  intopcoaconb  25643  isalg  25824  algi  25830  prismorcsetlem  26015  prismorcset  26017  dfiunv2  26019  iscola2  26195  abrexdom  26508  sdclem1  26556  sdc  26557  eq0rabdioph  26959  rexrabdioph  26978  eldioph4b  26997  hbtlem6  27436  dfaimafn2  28134  relopabVD  28993  bnj1146  29139  bnj1400  29184  bnj882  29274  bnj893  29276  psubspset  30555  pmapglb  30581  polval2N  30717  psubclsetN  30747  tendoset  31570
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289
  Copyright terms: Public domain W3C validator