Theorem rexlimiva 2609

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  ∃wrex 2476

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  unon  4548  reg2exmidlema  4571  ssfilem  6938  diffitest  6950  fival  7038  elfi2  7040  fi0  7043  djuss  7138  updjud  7150  enumct  7183  finnum  7252  dmaddpqlem  7447  nqpi  7448  nq0nn  7512  recexprlemm  7694  iswrd  10940  wrdf  10944  rexanuz  11156  r19.2uz  11161  maxleast  11381  fsum2dlemstep  11602  fisumcom2  11606  fprod2dlemstep  11790  fprodcom2fi  11794  0dvds  11979  even2n  12042  m1expe  12067  m1exp1  12069  modprm0  12434  gsumval2  13066  dfgrp2  13185  epttop  14352  neipsm  14416  tgioo  14816  sin0pilem2  15044  pilem3  15045  perfect  15263  bj-nn0suc  15636  bj-nn0sucALT  15650  trirec0xor  15716