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

Theorem r19.41v 2481
 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 1435 . 2 𝑥𝜓
21r19.41 2480 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
 Colors of variables: wff set class Syntax hints:   ∧ wa 101   ↔ wb 102  ∃wrex 2322 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-4 1414  ax-17 1433  ax-ial 1441 This theorem depends on definitions:  df-bi 114  df-nf 1364  df-rex 2327 This theorem is referenced by:  r19.42v  2482  3reeanv  2495  reuind  2764  iuncom4  3689  dfiun2g  3714  iunxiun  3761  inuni  3934  xpiundi  4423  xpiundir  4424  imaco  4851  coiun  4855  abrexco  5423  imaiun  5424  isoini  5482  rexrnmpt2  5641  genpassl  6650  genpassu  6651  4fvwrd4  9069
 Copyright terms: Public domain W3C validator