Theorem reximi2 3094

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

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1798   ∈ wcel 2141  ∃wrex 3085

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

This theorem depends on definitions:  df-bi 209  df-ex 1799  df-rex 3086

This theorem is referenced by:  reximia  3096  pssnn  9133  btwnz  12673  xrsupexmnf  13305  xrinfmexpnf  13306  xrsupsslem  13307  xrinfmsslem  13308  supxrun  13316  ioo0  13371  hashgt23el  14434  resqrex  15260  resqreu  15262  rexuzre  15363  neiptopnei  23172  comppfsc  23572  filssufilg  23951  alexsubALTlem4  24090  lgsquadlem2  27422  nmobndseqi  30928  nmobndseqiALT  30929  pjnmopi  32297  crefdf  34106  dya2iocuni  34541  ballotlemfc0  34751  ballotlemfcc  34752  ballotlemsup  34763  fnrelpredd  35351  poimirlem32  38115  sstotbnd3  38239  lsateln0  39583  pclcmpatN  40489  aaitgo  43703  stoweidlem14  46552  stoweidlem57  46595  elaa2  46772