Theorem reximi2 3095

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1811   ∈ wcel 2144  ∃wrex 3086

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

This proof depends on definitions:  df-bi 210  df-ex 1812  df-rex 3087

This theorem is used by:  reximia  3097  pssnn  9187  btwnz  12805  xrsupexmnf  13438  xrinfmexpnf  13439  xrsupsslem  13440  xrinfmsslem  13441  supxrun  13449  ioo0  13504  hashgt23el  14572  resqrex  15422  resqreu  15424  rexuzre  15525  neiptopnei  23455  comppfsc  23856  filssufilg  24235  alexsubALTlem4  24374  lgsquadlem2  27713  nmobndseqi  31386  nmobndseqiALT  31387  pjnmopi  32755  crefdf  34526  dya2iocuni  34961  ballotlemfc0  35171  ballotlemfcc  35172  ballotlemsup  35183  fnrelpredd  35772  poimirlem32  38663  sstotbnd3  38803  lsateln0  40145  pclcmpatN  41051  aaitgo  44257  stoweidlem14  47117  stoweidlem57  47160  elaa2  47337