Theorem reximi2 3066

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3057

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 3058

This theorem is referenced by:  reximia  3068  pssnn  9085  btwnz  12582  xrsupexmnf  13206  xrinfmexpnf  13207  xrsupsslem  13208  xrinfmsslem  13209  supxrun  13217  ioo0  13272  hashgt23el  14333  resqrex  15159  resqreu  15161  rexuzre  15262  neiptopnei  23048  comppfsc  23448  filssufilg  23827  alexsubALTlem4  23966  lgsquadlem2  27320  nmobndseqi  30761  nmobndseqiALT  30762  pjnmopi  32130  crefdf  33882  dya2iocuni  34317  ballotlemfc0  34527  ballotlemfcc  34528  ballotlemsup  34539  fnrelpredd  35123  poimirlem32  37712  sstotbnd3  37836  lsateln0  39114  pclcmpatN  40020  aaitgo  43279  stoweidlem14  46136  stoweidlem57  46179  elaa2  46356