Theorem rexlimiva 2578

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 2577	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2136  ∃wrex 2445

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-i5r 1523

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449  df-rex 2450

This theorem is referenced by:  unon  4488  reg2exmidlema  4511  ssfilem  6841  diffitest  6853  fival  6935  elfi2  6937  fi0  6940  djuss  7035  updjud  7047  enumct  7080  finnum  7139  dmaddpqlem  7318  nqpi  7319  nq0nn  7383  recexprlemm  7565  rexanuz  10930  r19.2uz  10935  maxleast  11155  fsum2dlemstep  11375  fisumcom2  11379  fprod2dlemstep  11563  fprodcom2fi  11567  0dvds  11751  even2n  11811  m1expe  11836  m1exp1  11838  modprm0  12186  epttop  12740  neipsm  12804  tgioo  13196  sin0pilem2  13353  pilem3  13354  bj-nn0suc  13856  bj-nn0sucALT  13870  trirec0xor  13934