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

Theorem 19.42v 1918
Description: Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.42v (∃𝑥(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem 19.42v
StepHypRef Expression
1 ax-17 1537 . 2 (𝜑 → ∀𝑥𝜑)
2119.42h 1698 1 (∃𝑥(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105  wex 1503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  exdistr  1921  19.42vv  1923  19.42vvv  1924  4exdistr  1928  cbvex2  1934  2sb5  1995  2sb5rf  2001  rexcom4a  2776  ceqsex2  2792  reuind  2957  2rmorex  2958  sbccomlem  3052  bm1.3ii  4139  opm  4249  eqvinop  4258  uniuni  4466  elco  4808  dmopabss  4854  dmopab3  4855  mptpreima  5137  brprcneu  5523  relelfvdm  5562  fndmin  5639  fliftf  5816  dfoprab2  5938  dmoprab  5972  dmoprabss  5973  fnoprabg  5992  opabex3d  6140  opabex3  6141  eroveu  6644  dmaddpq  7396  dmmulpq  7397  prarloc  7520  ltexprlemopl  7618  ltexprlemlol  7619  ltexprlemopu  7620  ltexprlemupu  7621  shftdm  10849  ntreq0  14029  bdbm1.3ii  15040
  Copyright terms: Public domain W3C validator