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  4511  reg2exmidlema  4534  ssfilem  6875  diffitest  6887  fival  6969  elfi2  6971  fi0  6974  djuss  7069  updjud  7081  enumct  7114  finnum  7182  dmaddpqlem  7376  nqpi  7377  nq0nn  7441  recexprlemm  7623  rexanuz  10997  r19.2uz  11002  maxleast  11222  fsum2dlemstep  11442  fisumcom2  11446  fprod2dlemstep  11630  fprodcom2fi  11634  0dvds  11818  even2n  11879  m1expe  11904  m1exp1  11906  modprm0  12254  dfgrp2  12902  epttop  13593  neipsm  13657  tgioo  14049  sin0pilem2  14206  pilem3  14207  bj-nn0suc  14719  bj-nn0sucALT  14733  trirec0xor  14796