| 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 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 4 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | |
| 5 | 2, 3, 4 | 3imtr4i 292 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∃wex 1779 ∈ wcel 2108 ∃wrex 3070 |
| 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 207 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: reximia 3081 pssnn 9208 btwnz 12721 xrsupexmnf 13347 xrinfmexpnf 13348 xrsupsslem 13349 xrinfmsslem 13350 supxrun 13358 ioo0 13412 hashgt23el 14463 resqrex 15289 resqreu 15291 rexuzre 15391 neiptopnei 23140 comppfsc 23540 filssufilg 23919 alexsubALTlem4 24058 lgsquadlem2 27425 nmobndseqi 30798 nmobndseqiALT 30799 pjnmopi 32167 crefdf 33847 dya2iocuni 34285 ballotlemfc0 34495 ballotlemfcc 34496 ballotlemsup 34507 fnrelpredd 35103 poimirlem32 37659 sstotbnd3 37783 lsateln0 38996 pclcmpatN 39903 aaitgo 43174 stoweidlem14 46029 stoweidlem57 46072 elaa2 46249 |
| Copyright terms: Public domain | W3C validator |