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  9105  btwnz  12607  xrsupexmnf  13232  xrinfmexpnf  13233  xrsupsslem  13234  xrinfmsslem  13235  supxrun  13243  ioo0  13298  hashgt23el  14359  resqrex  15185  resqreu  15187  rexuzre  15288  neiptopnei  23088  comppfsc  23488  filssufilg  23867  alexsubALTlem4  24006  lgsquadlem2  27360  nmobndseqi  30866  nmobndseqiALT  30867  pjnmopi  32235  crefdf  34025  dya2iocuni  34460  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemsup  34682  fnrelpredd  35266  poimirlem32  37897  sstotbnd3  38021  lsateln0  39365  pclcmpatN  40271  aaitgo  43513  stoweidlem14  46366  stoweidlem57  46409  elaa2  46586