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 1835	. 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 1779   ∈ wcel 2108  ∃wrex 3060

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 3061

This theorem is referenced by:  reximia  3071  pssnn  9182  btwnz  12696  xrsupexmnf  13321  xrinfmexpnf  13322  xrsupsslem  13323  xrinfmsslem  13324  supxrun  13332  ioo0  13387  hashgt23el  14442  resqrex  15269  resqreu  15271  rexuzre  15371  neiptopnei  23070  comppfsc  23470  filssufilg  23849  alexsubALTlem4  23988  lgsquadlem2  27344  nmobndseqi  30760  nmobndseqiALT  30761  pjnmopi  32129  crefdf  33879  dya2iocuni  34315  ballotlemfc0  34525  ballotlemfcc  34526  ballotlemsup  34537  fnrelpredd  35120  poimirlem32  37676  sstotbnd3  37800  lsateln0  39013  pclcmpatN  39920  aaitgo  43186  stoweidlem14  46043  stoweidlem57  46086  elaa2  46263