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 1842 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
3 | df-rex 3067 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | df-rex 3067 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | |
5 | 2, 3, 4 | 3imtr4i 295 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∃wex 1787 ∈ wcel 2110 ∃wrex 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 |
This theorem depends on definitions: df-bi 210 df-ex 1788 df-rex 3067 |
This theorem is referenced by: pssnn 8846 pssnnOLD 8895 btwnz 12279 xrsupexmnf 12895 xrinfmexpnf 12896 xrsupsslem 12897 xrinfmsslem 12898 supxrun 12906 ioo0 12960 hashgt23el 13991 resqrex 14814 resqreu 14816 rexuzre 14916 neiptopnei 22029 comppfsc 22429 filssufilg 22808 alexsubALTlem4 22947 lgsquadlem2 26262 nmobndseqi 28860 nmobndseqiALT 28861 pjnmopi 30229 crefdf 31512 dya2iocuni 31962 ballotlemfc0 32171 ballotlemfcc 32172 ballotlemsup 32183 fnrelpredd 32774 poimirlem32 35546 sstotbnd3 35671 lsateln0 36746 pclcmpatN 37652 aaitgo 40690 stoweidlem14 43230 stoweidlem57 43273 elaa2 43450 |
Copyright terms: Public domain | W3C validator |