Theorem rexlimiva 2589

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  ∃wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  unon  4512  reg2exmidlema  4535  ssfilem  6877  diffitest  6889  fival  6971  elfi2  6973  fi0  6976  djuss  7071  updjud  7083  enumct  7116  finnum  7184  dmaddpqlem  7378  nqpi  7379  nq0nn  7443  recexprlemm  7625  rexanuz  10999  r19.2uz  11004  maxleast  11224  fsum2dlemstep  11444  fisumcom2  11448  fprod2dlemstep  11632  fprodcom2fi  11636  0dvds  11820  even2n  11881  m1expe  11906  m1exp1  11908  modprm0  12256  dfgrp2  12907  epttop  13675  neipsm  13739  tgioo  14131  sin0pilem2  14288  pilem3  14289  bj-nn0suc  14801  bj-nn0sucALT  14815  trirec0xor  14878