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

Theorem exbii 1585
Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
Hypothesis
Ref Expression
exbii.1 (𝜑𝜓)
Assertion
Ref Expression
exbii (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Proof of Theorem exbii
StepHypRef Expression
1 exbi 1584 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2 exbii.1 . 2 (𝜑𝜓)
31, 2mpg 1428 1 (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  wex 1469
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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-ial 1515
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  2exbii  1586  3exbii  1587  exancom  1588  excom13  1668  exrot4  1670  eeor  1674  sbcof2  1783  sbequ8  1820  sbidm  1824  sborv  1863  19.41vv  1876  19.41vvv  1877  19.41vvvv  1878  exdistr  1882  19.42vvv  1885  exdistr2  1887  3exdistr  1888  4exdistr  1889  eean  1904  eeeanv  1906  ee4anv  1907  2sb5  1959  2sb5rf  1965  sbel2x  1974  sbexyz  1979  sbex  1980  exsb  1984  2exsb  1985  sb8eu  2013  sb8euh  2023  eu1  2025  eu2  2044  2moswapdc  2090  2exeu  2092  exists1  2096  clelab  2266  clabel  2267  sbabel  2308  rexbii2  2447  r2exf  2454  nfrexdya  2471  r19.41  2587  r19.43  2590  isset  2693  rexv  2705  ceqsex2  2727  ceqsex3v  2729  gencbvex  2733  ceqsrexv  2816  rexab  2847  rexrab2  2852  euxfrdc  2871  euind  2872  reu6  2874  reu3  2875  2reuswapdc  2889  reuind  2890  sbccomlem  2984  rmo2ilem  2999  rexun  3257  reupick3  3362  abn0r  3388  abn0m  3389  rabn0m  3391  rexsns  3566  exsnrex  3569  snprc  3592  euabsn2  3596  reusn  3598  eusn  3601  elunirab  3753  unipr  3754  uniun  3759  uniin  3760  iuncom4  3824  dfiun2g  3849  iunn0m  3877  iunxiun  3898  disjnim  3924  cbvopab2  4006  cbvopab2v  4009  unopab  4011  zfnuleu  4056  0ex  4059  vnex  4063  inex1  4066  intexabim  4081  iinexgm  4083  inuni  4084  unidif0  4095  axpweq  4099  zfpow  4103  axpow2  4104  axpow3  4105  vpwex  4107  zfpair2  4136  mss  4152  exss  4153  opm  4160  eqvinop  4169  copsexg  4170  opabm  4206  iunopab  4207  zfun  4360  uniex2  4362  uniuni  4376  rexxfrd  4388  dtruex  4478  zfinf2  4507  elxp2  4561  opeliunxp  4598  xpiundi  4601  xpiundir  4602  elvvv  4606  eliunxp  4682  rexiunxp  4685  relop  4693  elco  4709  opelco2g  4711  cnvco  4728  cnvuni  4729  dfdm3  4730  dfrn2  4731  dfrn3  4732  elrng  4734  dfdm4  4735  eldm2g  4739  dmun  4750  dmin  4751  dmiun  4752  dmuni  4753  dmopab  4754  dmi  4758  dmmrnm  4762  elrn  4786  rnopab  4790  dmcosseq  4814  dmres  4844  elres  4859  elsnres  4860  dfima2  4887  elima3  4892  imadmrn  4895  imai  4899  args  4912  rniun  4953  ssrnres  4985  dmsnm  5008  dmsnopg  5014  elxp4  5030  elxp5  5031  cnvresima  5032  mptpreima  5036  dfco2  5042  coundi  5044  coundir  5045  resco  5047  imaco  5048  rnco  5049  coiun  5052  coi1  5058  coass  5061  xpcom  5089  dffun2  5137  imadif  5207  imainlem  5208  funimaexglem  5210  fun11iun  5392  f11o  5404  brprcneu  5418  nfvres  5458  fndmin  5531  abrexco  5664  imaiun  5665  dfoprab2  5822  cbvoprab2  5848  rexrnmpo  5890  opabex3d  6023  opabex3  6024  abexssex  6027  abexex  6028  oprabrexex2  6032  releldm2  6087  dfopab2  6091  dfoprab3s  6092  cnvoprab  6135  brtpos2  6152  tfr1onlemaccex  6249  tfrcllembxssdm  6257  tfrcllemaccex  6262  domen  6649  mapsnen  6709  xpsnen  6719  xpcomco  6724  xpassen  6728  fimax2gtri  6799  supelti  6893  cc1  7093  subhalfnqq  7242  ltbtwnnq  7244  prnmaxl  7316  prnminu  7317  prarloc  7331  genpdflem  7335  genpassl  7352  genpassu  7353  ltexprlemm  7428  2rexuz  9400  seq3f1olemp  10302  cbvsum  11157  cbvprod  11355  inffinp1  11969  ctiunctal  11981  unct  11982  isbasis2g  12242  tgval2  12250  ntreq0  12331  lmff  12448  metrest  12705  bj-axempty  13245  bj-axempty2  13246  bj-vprc  13248  bdinex1  13251  bj-zfpair2  13262  bj-uniex2  13268  bj-d0clsepcl  13277
  Copyright terms: Public domain W3C validator