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

Theorem r19.41v 2466
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 1421 . 2 𝑥𝜓
21r19.41 2465 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wa 97  wb 98  wrex 2307
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  df-nf 1350  df-rex 2312
This theorem is referenced by:  r19.42v  2467  3reeanv  2480  reuind  2744  iuncom4  3664  dfiun2g  3689  iunxiun  3736  inuni  3909  xpiundi  4398  xpiundir  4399  imaco  4826  coiun  4830  abrexco  5398  imaiun  5399  isoini  5457  rexrnmpt2  5616  genpassl  6620  genpassu  6621  4fvwrd4  8995
  Copyright terms: Public domain W3C validator