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

Theorem abbii 2516
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 2514 . 2  |-  ( A. x ( ph  <->  ps )  <->  { x  |  ph }  =  { x  |  ps } )
2 abbii.1 . 2  |-  ( ph  <->  ps )
31, 2mpgbi 1555 1  |-  { x  |  ph }  =  {
x  |  ps }
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649   {cab 2390
This theorem is referenced by:  rabswap  2847  rabbiia  2906  rabab  2933  csb2  3213  cbvcsb  3215  csbid  3218  csbco  3220  cbvreucsf  3273  unrab  3572  inrab  3573  inrab2  3574  difrab  3575  rabun2  3580  dfnul3  3591  rab0  3608  dfif2  3701  tprot  3859  pw0  3905  pwpw0  3906  dfopif  3941  pwsn  3969  pwsnALT  3970  dfuni2  3977  unipr  3989  dfint2  4012  int0  4024  dfiunv2  4087  cbviun  4088  cbviin  4089  iunrab  4098  iunid  4106  viin  4110  iinuni  4134  cbvopab  4236  cbvopab1  4238  cbvopab2  4239  cbvopab1s  4240  cbvopab2v  4242  unopab  4244  zfrep4  4288  zfpair  4361  iunopab  4446  dfid3  4459  uniuni  4675  rabxp  4873  dfdm3  5017  dfrn2  5018  dfrn3  5019  dfdm4  5022  dfdmf  5023  dmun  5035  dmopab  5039  dmopabss  5040  dmopab3  5041  dfrnf  5067  rnopab  5074  rnmpt  5075  dfima2  5164  dfima3  5165  imadmrn  5174  imai  5177  args  5191  mptpreima  5322  dfiota2  5378  cbviota  5382  sb8iota  5384  dffv4  5684  dfimafn2  5735  fndmin  5796  fnasrn  5871  zfrep6  5927  fvresex  5941  elabrex  5944  abrexco  5945  abrexex2g  5947  abrexex2  5960  abexssex  5961  abexex  5962  dfoprab2  6080  cbvoprab2  6104  dmoprab  6113  rnoprab  6115  rnoprab2  6116  oprabrexex2  6148  fnrnov  6178  dfopab2  6360  opabiotadm  6496  rdglem1  6632  snec  6926  pmex  6982  dfixp  7024  cbvixp  7038  marypha2lem4  7401  ruv  7524  tcsni  7638  scottexs  7767  scott0s  7768  kardex  7774  cardf2  7786  dfac3  7958  infmap2  8054  cf0  8087  cfval2  8096  isf33lem  8202  dffin1-5  8224  axdc2lem  8284  addcompr  8854  mulcompr  8856  dfnn3  9970  hashf1lem2  11660  shftdm  11841  hashbc0  13328  efgval2  15311  dvdsrval  15705  dfrhm2  15776  tgval2  16976  tgdif0  17012  xkobval  17571  ustfn  18184  ustn0  18203  2sq  21113  vdgrun  21625  vdgrfiun  21626  nmopnegi  23421  nmop0  23442  nmfn0  23443  foo3  23899  abrexdomjm  23941  abrexexd  23943  dfimafnf  23996  mptfnf  24026  ofpreima  24034  hasheuni  24428  sigaex  24445  sigaval  24446  isrnsigaOLD  24448  ballotlem2  24699  derang0  24808  subfaclefac  24815  dfon2lem7  25359  dfon2  25362  domep  25363  dfrdg2  25366  poseq  25467  soseq  25468  tfrALTlem  25490  dfiota3  25676  fvline  25982  ellines  25990  rabiun2  26139  ismblfin  26146  volsupnfl  26150  areacirclem6  26186  abrexdom  26322  sdclem1  26337  sdc  26338  eq0rabdioph  26725  rexrabdioph  26744  eldioph4b  26762  hbtlem6  27201  dfaimafn2  27897  relopabVD  28722  bnj1146  28868  bnj1400  28913  bnj882  29003  bnj893  29005  psubspset  30226  pmapglb  30252  polval2N  30388  psubclsetN  30418  tendoset  31241
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397
  Copyright terms: Public domain W3C validator