Theorem rexlimiva 2606

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164  ∃wrex 2473

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477  df-rex 2478

This theorem is referenced by:  unon  4544  reg2exmidlema  4567  ssfilem  6933  diffitest  6945  fival  7031  elfi2  7033  fi0  7036  djuss  7131  updjud  7143  enumct  7176  finnum  7245  dmaddpqlem  7439  nqpi  7440  nq0nn  7504  recexprlemm  7686  iswrd  10919  wrdf  10923  rexanuz  11135  r19.2uz  11140  maxleast  11360  fsum2dlemstep  11580  fisumcom2  11584  fprod2dlemstep  11768  fprodcom2fi  11772  0dvds  11957  even2n  12018  m1expe  12043  m1exp1  12045  modprm0  12395  gsumval2  12983  dfgrp2  13102  epttop  14269  neipsm  14333  tgioo  14733  sin0pilem2  14958  pilem3  14959  bj-nn0suc  15526  bj-nn0sucALT  15540  trirec0xor  15605