Theorem reximi2 3010

Description: Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.)

Hypothesis

Ref	Expression
reximi2.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓))

Assertion

Ref	Expression
reximi2	⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Proof of Theorem reximi2

Step	Hyp	Ref	Expression
1		reximi2.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓))
2	1	eximi 1762	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))
3		df-rex 2918	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rex 2918	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))
5	2, 3, 4	3imtr4i 281	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 384  ∃wex 1704   ∈ wcel 1990  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-rex 2918

This theorem is referenced by:  pssnn  8178  btwnz  11479  xrsupexmnf  12135  xrinfmexpnf  12136  xrsupsslem  12137  xrinfmsslem  12138  supxrun  12146  ioo0  12200  resqrex  13991  resqreu  13993  rexuzre  14092  neiptopnei  20936  comppfsc  21335  filssufilg  21715  alexsubALTlem4  21854  lgsquadlem2  25106  nmobndseqi  27634  nmobndseqiALT  27635  pjnmopi  29007  crefdf  29915  dya2iocuni  30345  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemsup  30566  poimirlem32  33441  sstotbnd3  33575  lsateln0  34282  pclcmpatN  35187  aaitgo  37732  stoweidlem14  40231  stoweidlem57  40274  elaa2  40451