Theorem reximi2 3098

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400  ∃wex 1809   ∈ wcel 2143  ∃wrex 3089

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

This proof depends on definitions:  df-bi 210  df-ex 1810  df-rex 3090

This theorem is used by:  reximia  3100  pssnn  9149  btwnz  12703  xrsupexmnf  13335  xrinfmexpnf  13336  xrsupsslem  13337  xrinfmsslem  13338  supxrun  13346  ioo0  13401  hashgt23el  14466  resqrex  15306  resqreu  15308  rexuzre  15409  neiptopnei  23298  comppfsc  23698  filssufilg  24077  alexsubALTlem4  24216  lgsquadlem2  27554  nmobndseqi  31140  nmobndseqiALT  31141  pjnmopi  32509  crefdf  34247  dya2iocuni  34682  ballotlemfc0  34892  ballotlemfcc  34893  ballotlemsup  34904  fnrelpredd  35491  poimirlem32  38331  sstotbnd3  38455  lsateln0  39797  pclcmpatN  40703  aaitgo  43917  stoweidlem14  46756  stoweidlem57  46799  elaa2  46976