Theorem reximi2 3085

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 1833	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))
3		df-rex 3077	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rex 3077	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))
5	2, 3, 4	3imtr4i 292	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1777   ∈ wcel 2108  ∃wrex 3076

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

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-rex 3077

This theorem is referenced by:  reximia  3087  pssnn  9234  btwnz  12746  xrsupexmnf  13367  xrinfmexpnf  13368  xrsupsslem  13369  xrinfmsslem  13370  supxrun  13378  ioo0  13432  hashgt23el  14473  resqrex  15299  resqreu  15301  rexuzre  15401  neiptopnei  23161  comppfsc  23561  filssufilg  23940  alexsubALTlem4  24079  lgsquadlem2  27443  nmobndseqi  30811  nmobndseqiALT  30812  pjnmopi  32180  crefdf  33794  dya2iocuni  34248  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemsup  34469  fnrelpredd  35065  poimirlem32  37612  sstotbnd3  37736  lsateln0  38951  pclcmpatN  39858  aaitgo  43119  stoweidlem14  45935  stoweidlem57  45978  elaa2  46155