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 1835 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
3 | df-rex 3072 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | df-rex 3072 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | |
5 | 2, 3, 4 | 3imtr4i 293 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∃wex 1779 ∈ wcel 2104 ∃wrex 3071 |
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 206 df-ex 1780 df-rex 3072 |
This theorem is referenced by: reximia 3081 pssnn 8985 pssnnOLD 9080 btwnz 12465 xrsupexmnf 13081 xrinfmexpnf 13082 xrsupsslem 13083 xrinfmsslem 13084 supxrun 13092 ioo0 13146 hashgt23el 14180 resqrex 15003 resqreu 15005 rexuzre 15105 neiptopnei 22324 comppfsc 22724 filssufilg 23103 alexsubALTlem4 23242 lgsquadlem2 26570 nmobndseqi 29182 nmobndseqiALT 29183 pjnmopi 30551 crefdf 31839 dya2iocuni 32291 ballotlemfc0 32500 ballotlemfcc 32501 ballotlemsup 32512 fnrelpredd 33102 poimirlem32 35850 sstotbnd3 35975 lsateln0 37048 pclcmpatN 37954 aaitgo 41024 stoweidlem14 43603 stoweidlem57 43646 elaa2 43823 |
Copyright terms: Public domain | W3C validator |