Theorem reximi2 3097

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813  df-rex 3089

This theorem is used by:  reximia  3099  pssnn  9167  btwnz  12728  xrsupexmnf  13361  xrinfmexpnf  13362  xrsupsslem  13363  xrinfmsslem  13364  supxrun  13372  ioo0  13427  hashgt23el  14493  resqrex  15341  resqreu  15343  rexuzre  15444  neiptopnei  23363  comppfsc  23764  filssufilg  24143  alexsubALTlem4  24282  lgsquadlem2  27625  nmobndseqi  31268  nmobndseqiALT  31269  pjnmopi  32637  crefdf  34366  dya2iocuni  34802  ballotlemfc0  35012  ballotlemfcc  35013  ballotlemsup  35024  fnrelpredd  35604  poimirlem32  38409  sstotbnd3  38534  lsateln0  39876  pclcmpatN  40782  aaitgo  44011  stoweidlem14  46850  stoweidlem57  46893  elaa2  47070