Theorem rexlimiva 2518

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 114	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	rexlimiv 2517	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1463  ∃wrex 2391

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-i5r 1498

This theorem depends on definitions:  df-bi 116  df-nf 1420  df-ral 2395  df-rex 2396

This theorem is referenced by:  unon  4387  reg2exmidlema  4409  ssfilem  6722  diffitest  6734  fival  6810  elfi2  6812  fi0  6815  djuss  6907  updjud  6919  enumct  6952  finnum  6989  dmaddpqlem  7133  nqpi  7134  nq0nn  7198  recexprlemm  7380  rexanuz  10652  r19.2uz  10657  maxleast  10877  fsum2dlemstep  11095  fisumcom2  11099  0dvds  11361  even2n  11419  m1expe  11444  m1exp1  11446  epttop  12102  neipsm  12166  tgioo  12532  bj-nn0suc  12854  bj-nn0sucALT  12868