Theorem reximi2 3070

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3061

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

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-rex 3062

This theorem is referenced by:  reximia  3072  pssnn  9103  btwnz  12632  xrsupexmnf  13257  xrinfmexpnf  13258  xrsupsslem  13259  xrinfmsslem  13260  supxrun  13268  ioo0  13323  hashgt23el  14386  resqrex  15212  resqreu  15214  rexuzre  15315  neiptopnei  23097  comppfsc  23497  filssufilg  23876  alexsubALTlem4  24015  lgsquadlem2  27344  nmobndseqi  30850  nmobndseqiALT  30851  pjnmopi  32219  crefdf  33992  dya2iocuni  34427  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemsup  34649  fnrelpredd  35234  poimirlem32  37973  sstotbnd3  38097  lsateln0  39441  pclcmpatN  40347  aaitgo  43590  stoweidlem14  46442  stoweidlem57  46485  elaa2  46662