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 1835	. 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 1779   ∈ wcel 2109  ∃wrex 3054

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

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

This theorem is referenced by:  reximia  3065  pssnn  9138  btwnz  12644  xrsupexmnf  13272  xrinfmexpnf  13273  xrsupsslem  13274  xrinfmsslem  13275  supxrun  13283  ioo0  13338  hashgt23el  14396  resqrex  15223  resqreu  15225  rexuzre  15326  neiptopnei  23026  comppfsc  23426  filssufilg  23805  alexsubALTlem4  23944  lgsquadlem2  27299  nmobndseqi  30715  nmobndseqiALT  30716  pjnmopi  32084  crefdf  33845  dya2iocuni  34281  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemsup  34503  fnrelpredd  35086  poimirlem32  37653  sstotbnd3  37777  lsateln0  38995  pclcmpatN  39902  aaitgo  43158  stoweidlem14  46019  stoweidlem57  46062  elaa2  46239