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

Theorem 19.42v 1786
 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 1419 . 2 (𝜑 → ∀𝑥𝜑)
2119.42h 1577 1 (∃𝑥(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98  ∃wex 1381 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  exdistr  1787  19.42vv  1788  19.42vvv  1789  4exdistr  1793  cbvex2  1797  2sb5  1859  2sb5rf  1865  rexcom4a  2578  ceqsex2  2594  reuind  2744  2rmorex  2745  sbccomlem  2832  bm1.3ii  3878  opm  3971  eqvinop  3980  uniuni  4183  dmopabss  4547  dmopab3  4548  mptpreima  4814  brprcneu  5171  relelfvdm  5205  fndmin  5274  fliftf  5439  dfoprab2  5552  dmoprab  5585  dmoprabss  5586  fnoprabg  5602  opabex3d  5748  opabex3  5749  eroveu  6197  dmaddpq  6477  dmmulpq  6478  prarloc  6601  ltexprlemopl  6699  ltexprlemlol  6700  ltexprlemopu  6701  ltexprlemupu  6702  shftdm  9423  bdbm1.3ii  10011
 Copyright terms: Public domain W3C validator