Theorem rexlimiva 2609

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.)

Hypothesis

Ref	Expression
rexlimiva.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)

Assertion

Ref	Expression
rexlimiva	⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimiva

Step	Hyp	Ref	Expression
1		rexlimiva.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
2	1	ex 115	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	rexlimiv 2608	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  ∃wrex 2476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  unon  4548  reg2exmidlema  4571  ssfilem  6945  diffitest  6957  fival  7045  elfi2  7047  fi0  7050  djuss  7145  updjud  7157  enumct  7190  finnum  7263  dmaddpqlem  7463  nqpi  7464  nq0nn  7528  recexprlemm  7710  iswrd  10956  wrdf  10960  rexanuz  11172  r19.2uz  11177  maxleast  11397  fsum2dlemstep  11618  fisumcom2  11622  fprod2dlemstep  11806  fprodcom2fi  11810  0dvds  11995  even2n  12058  m1expe  12083  m1exp1  12085  modprm0  12450  gsumval2  13101  dfgrp2  13231  epttop  14434  neipsm  14498  tgioo  14898  sin0pilem2  15126  pilem3  15127  perfect  15345  bj-nn0suc  15718  bj-nn0sucALT  15732  trirec0xor  15802