ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exbii Unicode version

Theorem exbii 1512
Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
Hypothesis
Ref Expression
exbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
exbii  |-  ( E. x ph  <->  E. x ps )

Proof of Theorem exbii
StepHypRef Expression
1 exbi 1511 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  <->  E. x ps ) )
2 exbii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1356 1  |-  ( E. x ph  <->  E. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 102   E.wex 1397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-ial 1443
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  2exbii  1513  3exbii  1514  exancom  1515  excom13  1595  exrot4  1597  eeor  1601  sbcof2  1707  sbequ8  1743  sbidm  1747  sborv  1786  19.41vv  1799  19.41vvv  1800  19.41vvvv  1801  exdistr  1803  19.42vvv  1805  exdistr2  1807  3exdistr  1808  4exdistr  1809  eean  1822  eeeanv  1824  ee4anv  1825  2sb5  1875  2sb5rf  1881  sbel2x  1890  sbexyz  1895  sbex  1896  exsb  1900  2exsb  1901  sb8eu  1929  sb8euh  1939  eu1  1941  eu2  1960  2moswapdc  2006  2exeu  2008  exists1  2012  clelab  2178  clabel  2179  sbabel  2219  rexbii2  2352  r2exf  2359  nfrexdya  2376  r19.41  2482  r19.43  2485  isset  2578  rexv  2589  ceqsex2  2611  ceqsex3v  2613  gencbvex  2617  ceqsrexv  2697  rexab  2726  rexrab2  2731  euxfrdc  2750  euind  2751  reu6  2753  reu3  2754  2reuswapdc  2766  reuind  2767  sbccomlem  2860  rmo2ilem  2875  rexun  3151  reupick3  3250  abn0r  3271  rabn0m  3273  rexsns  3437  rexsnsOLD  3438  exsnrex  3441  snprc  3463  euabsn2  3467  reusn  3469  eusn  3472  elunirab  3621  unipr  3622  uniun  3627  uniin  3628  iuncom4  3692  dfiun2g  3717  iunn0m  3745  iunxiun  3764  cbvopab2  3859  cbvopab2v  3862  unopab  3864  zfnuleu  3909  0ex  3912  vprc  3916  inex1  3919  intexabim  3934  iinexgm  3936  inuni  3937  unidif0  3948  axpweq  3952  zfpow  3956  axpow2  3957  axpow3  3958  pwex  3960  zfpair2  3973  mss  3990  exss  3991  opm  3999  eqvinop  4008  copsexg  4009  opabm  4045  iunopab  4046  zfun  4199  uniex2  4201  uniuni  4211  rexxfrd  4223  dtruex  4311  zfinf2  4340  elxp2  4391  opeliunxp  4423  xpiundi  4426  xpiundir  4427  elvvv  4431  eliunxp  4503  rexiunxp  4506  relop  4514  opelco2g  4531  cnvco  4548  cnvuni  4549  dfdm3  4550  dfrn2  4551  dfrn3  4552  elrng  4554  dfdm4  4555  eldm2g  4559  dmun  4570  dmin  4571  dmiun  4572  dmuni  4573  dmopab  4574  dmi  4578  dmmrnm  4582  elrn  4605  rnopab  4609  dmcosseq  4631  dmres  4660  elres  4674  elsnres  4675  dfima2  4698  elima3  4703  imadmrn  4706  imai  4709  args  4722  rniun  4762  ssrnres  4791  dmsnm  4814  dmsnopg  4820  elxp4  4836  elxp5  4837  cnvresima  4838  mptpreima  4842  dfco2  4848  coundi  4850  coundir  4851  resco  4853  imaco  4854  rnco  4855  coiun  4858  coi1  4864  coass  4867  xpcom  4892  dffun2  4940  imadif  5007  imainlem  5008  funimaexglem  5010  fun11iun  5175  f11o  5187  brprcneu  5199  nfvres  5234  fndmin  5302  abrexco  5426  imaiun  5427  dfoprab2  5580  cbvoprab2  5605  rexrnmpt2  5644  opabex3d  5776  opabex3  5777  abexssex  5780  abexex  5781  oprabrexex2  5785  releldm2  5839  dfopab2  5843  dfoprab3s  5844  cnvoprab  5883  brtpos2  5897  domen  6263  xpsnen  6326  xpcomco  6331  xpassen  6335  subhalfnqq  6570  ltbtwnnq  6572  prnmaxl  6644  prnminu  6645  prarloc  6659  genpdflem  6663  genpassl  6680  genpassu  6681  ltexprlemm  6756  2rexuz  8621  bj-axempty  10400  bj-axempty2  10401  bj-vprc  10403  bdinex1  10406  bj-zfpair2  10417  bj-uniex2  10423  bj-d0clsepcl  10436
  Copyright terms: Public domain W3C validator