Theorem reximi2 3069

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3060

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 3061

This theorem is referenced by:  reximia  3071  pssnn  9093  btwnz  12595  xrsupexmnf  13220  xrinfmexpnf  13221  xrsupsslem  13222  xrinfmsslem  13223  supxrun  13231  ioo0  13286  hashgt23el  14347  resqrex  15173  resqreu  15175  rexuzre  15276  neiptopnei  23076  comppfsc  23476  filssufilg  23855  alexsubALTlem4  23994  lgsquadlem2  27348  nmobndseqi  30854  nmobndseqiALT  30855  pjnmopi  32223  crefdf  34005  dya2iocuni  34440  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemsup  34662  fnrelpredd  35247  poimirlem32  37849  sstotbnd3  37973  lsateln0  39251  pclcmpatN  40157  aaitgo  43400  stoweidlem14  46254  stoweidlem57  46297  elaa2  46474