Theorem reximi2 3077

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1776   ∈ wcel 2106  ∃wrex 3068

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

This theorem depends on definitions:  df-bi 207  df-ex 1777  df-rex 3069

This theorem is referenced by:  reximia  3079  pssnn  9207  btwnz  12719  xrsupexmnf  13344  xrinfmexpnf  13345  xrsupsslem  13346  xrinfmsslem  13347  supxrun  13355  ioo0  13409  hashgt23el  14460  resqrex  15286  resqreu  15288  rexuzre  15388  neiptopnei  23156  comppfsc  23556  filssufilg  23935  alexsubALTlem4  24074  lgsquadlem2  27440  nmobndseqi  30808  nmobndseqiALT  30809  pjnmopi  32177  crefdf  33809  dya2iocuni  34265  ballotlemfc0  34474  ballotlemfcc  34475  ballotlemsup  34486  fnrelpredd  35082  poimirlem32  37639  sstotbnd3  37763  lsateln0  38977  pclcmpatN  39884  aaitgo  43151  stoweidlem14  45970  stoweidlem57  46013  elaa2  46190