![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reximi2 | Structured version Visualization version GIF version |
Description: Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.) |
Ref | Expression |
---|---|
reximi2.1 | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓)) |
Ref | Expression |
---|---|
reximi2 | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximi2.1 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓)) | |
2 | 1 | eximi 1797 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
3 | df-rex 3088 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | df-rex 3088 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | |
5 | 2, 3, 4 | 3imtr4i 284 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∃wex 1742 ∈ wcel 2048 ∃wrex 3083 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 |
This theorem depends on definitions: df-bi 199 df-ex 1743 df-rex 3088 |
This theorem is referenced by: pssnn 8523 btwnz 11890 xrsupexmnf 12507 xrinfmexpnf 12508 xrsupsslem 12509 xrinfmsslem 12510 supxrun 12518 ioo0 12572 resqrex 14461 resqreu 14463 rexuzre 14563 neiptopnei 21434 comppfsc 21834 filssufilg 22213 alexsubALTlem4 22352 lgsquadlem2 25649 nmobndseqi 28323 nmobndseqiALT 28324 pjnmopi 29696 crefdf 30713 dya2iocuni 31143 ballotlemfc0 31353 ballotlemfcc 31354 ballotlemsup 31365 poimirlem32 34313 sstotbnd3 34444 lsateln0 35524 pclcmpatN 36430 aaitgo 39103 stoweidlem14 41676 stoweidlem57 41719 elaa2 41896 |
Copyright terms: Public domain | W3C validator |