![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reximdv2 | Structured version Visualization version GIF version |
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.) |
Ref | Expression |
---|---|
reximdv2.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒))) |
Ref | Expression |
---|---|
reximdv2 | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximdv2.1 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒))) | |
2 | 1 | eximdv 1960 | . 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))) |
3 | df-rex 3095 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
4 | df-rex 3095 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)) | |
5 | 2, 3, 4 | 3imtr4g 288 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∃wex 1823 ∈ wcel 2106 ∃wrex 3090 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 |
This theorem depends on definitions: df-bi 199 df-ex 1824 df-rex 3095 |
This theorem is referenced by: reximssdv 3199 ssrexv 3885 ssimaex 6523 nnsuc 7360 oaass 7925 omeulem1 7946 ssnnfi 8467 findcard3 8491 unfilem1 8512 epfrs 8904 alephval3 9266 isfin7-2 9553 fpwwe2lem13 9799 inawinalem 9846 ico0 12533 ioc0 12534 r19.2uz 14498 climrlim2 14686 iserodd 15944 ramub2 16122 prmgaplem6 16164 ablfaclem3 18873 unitgrp 19054 restnlly 21694 llyrest 21697 nllyrest 21698 llyidm 21700 nllyidm 21701 cnpflfi 22211 cnextcn 22279 ivthlem3 23657 dvfsumrlim 24231 lgsquadlem2 25558 footex 26069 oppperpex 26101 outpasch 26103 ushgredgedg 26575 ushgredgedgloop 26577 ushgredgedgloopOLD 26578 cusgrfilem2 26804 cmppcmp 30523 eulerpartlemgvv 31036 eulerpartlemgh 31038 erdszelem7 31778 rellysconn 31832 trpredrec 32326 ivthALT 32918 fnessref 32940 phpreu 34002 poimirlem26 34045 itg2gt0cn 34074 frinfm 34139 sstotbnd2 34181 heiborlem3 34220 isdrngo3 34366 dihjat1lem 37566 dvh1dim 37580 dochsatshp 37589 mapdpglem2 37811 pellexlem5 38339 pell14qrss1234 38362 pell1qrss14 38374 lnr2i 38627 hbtlem6 38640 |
Copyright terms: Public domain | W3C validator |