Theorem rexlimiva 2645

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ∃wrex 2511

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  unon  4609  reg2exmidlema  4632  ssfilem  7065  ssfilemd  7067  diffitest  7079  fival  7172  elfi2  7174  fi0  7177  djuss  7272  updjud  7284  enumct  7317  finnum  7390  dmaddpqlem  7600  nqpi  7601  nq0nn  7665  recexprlemm  7847  iswrd  11122  wrdf  11126  rexanuz  11569  r19.2uz  11574  maxleast  11794  fsum2dlemstep  12016  fisumcom2  12020  fprod2dlemstep  12204  fprodcom2fi  12208  0dvds  12393  even2n  12456  m1expe  12481  m1exp1  12483  modprm0  12848  gsumval2  13501  dfgrp2  13631  epttop  14841  neipsm  14905  tgioo  15305  sin0pilem2  15533  pilem3  15534  perfect  15752  clwwlkn1loopb  16298  bj-nn0suc  16618  bj-nn0sucALT  16632  trirec0xor  16708