Theorem reximi2 3065

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2111  ∃wrex 3056

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 3057

This theorem is referenced by:  reximia  3067  pssnn  9078  btwnz  12573  xrsupexmnf  13201  xrinfmexpnf  13202  xrsupsslem  13203  xrinfmsslem  13204  supxrun  13212  ioo0  13267  hashgt23el  14328  resqrex  15154  resqreu  15156  rexuzre  15257  neiptopnei  23045  comppfsc  23445  filssufilg  23824  alexsubALTlem4  23963  lgsquadlem2  27317  nmobndseqi  30754  nmobndseqiALT  30755  pjnmopi  32123  crefdf  33856  dya2iocuni  34291  ballotlemfc0  34501  ballotlemfcc  34502  ballotlemsup  34513  fnrelpredd  35097  poimirlem32  37691  sstotbnd3  37815  lsateln0  39033  pclcmpatN  39939  aaitgo  43194  stoweidlem14  46051  stoweidlem57  46094  elaa2  46271