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

Theorem 19.42v 1862
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 1491 . 2 (𝜑 → ∀𝑥𝜑)
2119.42h 1650 1 (∃𝑥(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104  wex 1453
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  exdistr  1863  19.42vv  1865  19.42vvv  1866  4exdistr  1870  cbvex2  1874  2sb5  1936  2sb5rf  1942  rexcom4a  2684  ceqsex2  2700  reuind  2862  2rmorex  2863  sbccomlem  2955  bm1.3ii  4019  opm  4126  eqvinop  4135  uniuni  4342  elco  4675  dmopabss  4721  dmopab3  4722  mptpreima  5002  brprcneu  5382  relelfvdm  5421  fndmin  5495  fliftf  5668  dfoprab2  5786  dmoprab  5820  dmoprabss  5821  fnoprabg  5840  opabex3d  5987  opabex3  5988  eroveu  6488  dmaddpq  7155  dmmulpq  7156  prarloc  7279  ltexprlemopl  7377  ltexprlemlol  7378  ltexprlemopu  7379  ltexprlemupu  7380  shftdm  10562  ntreq0  12228  bdbm1.3ii  13016
  Copyright terms: Public domain W3C validator