Theorem reximi2 3063

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2110  ∃wrex 3054

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

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-rex 3055

This theorem is referenced by:  reximia  3065  pssnn  9073  btwnz  12568  xrsupexmnf  13196  xrinfmexpnf  13197  xrsupsslem  13198  xrinfmsslem  13199  supxrun  13207  ioo0  13262  hashgt23el  14323  resqrex  15149  resqreu  15151  rexuzre  15252  neiptopnei  23040  comppfsc  23440  filssufilg  23819  alexsubALTlem4  23958  lgsquadlem2  27312  nmobndseqi  30749  nmobndseqiALT  30750  pjnmopi  32118  crefdf  33851  dya2iocuni  34286  ballotlemfc0  34496  ballotlemfcc  34497  ballotlemsup  34508  fnrelpredd  35091  poimirlem32  37671  sstotbnd3  37795  lsateln0  39013  pclcmpatN  39919  aaitgo  43174  stoweidlem14  46031  stoweidlem57  46074  elaa2  46251