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

Theorem r19.41v 2585
 Description: Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 17-Dec-2003.)
Assertion
Ref Expression
r19.41v (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Distinct variable group:   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem r19.41v
StepHypRef Expression
1 nfv 1508 . 2 𝑥𝜓
21r19.41 2584 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104  ∃wrex 2415 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-17 1506  ax-ial 1514 This theorem depends on definitions:  df-bi 116  df-nf 1437  df-rex 2420 This theorem is referenced by:  r19.42v  2586  3reeanv  2599  reuind  2884  iuncom4  3815  dfiun2g  3840  iunxiun  3889  inuni  4075  xpiundi  4592  xpiundir  4593  imaco  5039  coiun  5043  abrexco  5653  imaiun  5654  isoini  5712  rexrnmpo  5879  mapsnen  6698  genpassl  7325  genpassu  7326  4fvwrd4  9910  metrest  12664
 Copyright terms: Public domain W3C validator