Theorem reximi2 3071

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

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

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 3063

This theorem is referenced by:  reximia  3073  pssnn  9096  btwnz  12623  xrsupexmnf  13248  xrinfmexpnf  13249  xrsupsslem  13250  xrinfmsslem  13251  supxrun  13259  ioo0  13314  hashgt23el  14377  resqrex  15203  resqreu  15205  rexuzre  15306  neiptopnei  23107  comppfsc  23507  filssufilg  23886  alexsubALTlem4  24025  lgsquadlem2  27358  nmobndseqi  30865  nmobndseqiALT  30866  pjnmopi  32234  crefdf  34008  dya2iocuni  34443  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemsup  34665  fnrelpredd  35250  poimirlem32  37987  sstotbnd3  38111  lsateln0  39455  pclcmpatN  40361  aaitgo  43608  stoweidlem14  46460  stoweidlem57  46503  elaa2  46680