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

Theorem exbii 1584
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 1583 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  <->  E. x ps ) )
2 exbii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1427 1  |-  ( E. x ph  <->  E. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   E.wex 1468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  2exbii  1585  3exbii  1586  exancom  1587  excom13  1667  exrot4  1669  eeor  1673  sbcof2  1782  sbequ8  1819  sbidm  1823  sborv  1862  19.41vv  1875  19.41vvv  1876  19.41vvvv  1877  exdistr  1881  19.42vvv  1884  exdistr2  1886  3exdistr  1887  4exdistr  1888  eean  1901  eeeanv  1903  ee4anv  1904  2sb5  1956  2sb5rf  1962  sbel2x  1971  sbexyz  1976  sbex  1977  exsb  1981  2exsb  1982  sb8eu  2010  sb8euh  2020  eu1  2022  eu2  2041  2moswapdc  2087  2exeu  2089  exists1  2093  clelab  2263  clabel  2264  sbabel  2305  rexbii2  2444  r2exf  2451  nfrexdya  2468  r19.41  2584  r19.43  2587  isset  2687  rexv  2699  ceqsex2  2721  ceqsex3v  2723  gencbvex  2727  ceqsrexv  2810  rexab  2841  rexrab2  2846  euxfrdc  2865  euind  2866  reu6  2868  reu3  2869  2reuswapdc  2883  reuind  2884  sbccomlem  2978  rmo2ilem  2993  rexun  3251  reupick3  3356  abn0r  3382  abn0m  3383  rabn0m  3385  rexsns  3558  exsnrex  3561  snprc  3583  euabsn2  3587  reusn  3589  eusn  3592  elunirab  3744  unipr  3745  uniun  3750  uniin  3751  iuncom4  3815  dfiun2g  3840  iunn0m  3868  iunxiun  3889  disjnim  3915  cbvopab2  3997  cbvopab2v  4000  unopab  4002  zfnuleu  4047  0ex  4050  vnex  4054  inex1  4057  intexabim  4072  iinexgm  4074  inuni  4075  unidif0  4086  axpweq  4090  zfpow  4094  axpow2  4095  axpow3  4096  vpwex  4098  zfpair2  4127  mss  4143  exss  4144  opm  4151  eqvinop  4160  copsexg  4161  opabm  4197  iunopab  4198  zfun  4351  uniex2  4353  uniuni  4367  rexxfrd  4379  dtruex  4469  zfinf2  4498  elxp2  4552  opeliunxp  4589  xpiundi  4592  xpiundir  4593  elvvv  4597  eliunxp  4673  rexiunxp  4676  relop  4684  elco  4700  opelco2g  4702  cnvco  4719  cnvuni  4720  dfdm3  4721  dfrn2  4722  dfrn3  4723  elrng  4725  dfdm4  4726  eldm2g  4730  dmun  4741  dmin  4742  dmiun  4743  dmuni  4744  dmopab  4745  dmi  4749  dmmrnm  4753  elrn  4777  rnopab  4781  dmcosseq  4805  dmres  4835  elres  4850  elsnres  4851  dfima2  4878  elima3  4883  imadmrn  4886  imai  4890  args  4903  rniun  4944  ssrnres  4976  dmsnm  4999  dmsnopg  5005  elxp4  5021  elxp5  5022  cnvresima  5023  mptpreima  5027  dfco2  5033  coundi  5035  coundir  5036  resco  5038  imaco  5039  rnco  5040  coiun  5043  coi1  5049  coass  5052  xpcom  5080  dffun2  5128  imadif  5198  imainlem  5199  funimaexglem  5201  fun11iun  5381  f11o  5393  brprcneu  5407  nfvres  5447  fndmin  5520  abrexco  5653  imaiun  5654  dfoprab2  5811  cbvoprab2  5837  rexrnmpo  5879  opabex3d  6012  opabex3  6013  abexssex  6016  abexex  6017  oprabrexex2  6021  releldm2  6076  dfopab2  6080  dfoprab3s  6081  cnvoprab  6124  brtpos2  6141  tfr1onlemaccex  6238  tfrcllembxssdm  6246  tfrcllemaccex  6251  domen  6638  mapsnen  6698  xpsnen  6708  xpcomco  6713  xpassen  6717  fimax2gtri  6788  supelti  6882  subhalfnqq  7215  ltbtwnnq  7217  prnmaxl  7289  prnminu  7290  prarloc  7304  genpdflem  7308  genpassl  7325  genpassu  7326  ltexprlemm  7401  2rexuz  9370  seq3f1olemp  10268  cbvsum  11122  cbvprod  11320  inffinp1  11927  unct  11939  isbasis2g  12197  tgval2  12205  ntreq0  12286  lmff  12403  metrest  12660  bj-axempty  13076  bj-axempty2  13077  bj-vprc  13079  bdinex1  13082  bj-zfpair2  13093  bj-uniex2  13099  bj-d0clsepcl  13108
  Copyright terms: Public domain W3C validator