| 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 1917 | . 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))) |
| 3 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
| 4 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)) | |
| 5 | 2, 3, 4 | 3imtr4g 296 | 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 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: reximdvai 3165 reximssdv 3173 ssrexvOLD 4057 ssimaex 6994 nnsuc 7905 oaass 8599 omeulem1 8620 ssnnfi 9209 findcard3 9318 findcard3OLD 9319 unfilem1 9343 epfrs 9771 alephval3 10150 isfin7-2 10436 fpwwe2lem12 10682 inawinalem 10729 ico0 13433 ioc0 13434 r19.2uz 15390 climrlim2 15583 prmdvdsncoprmbd 16764 iserodd 16873 ramub2 17052 prmgaplem6 17094 ghmqusnsglem2 19299 ghmquskerlem2 19303 ablfaclem3 20107 unitgrp 20383 restnlly 23490 llyrest 23493 nllyrest 23494 llyidm 23496 nllyidm 23497 cnpflfi 24007 cnextcn 24075 ivthlem3 25488 dvfsumrlim 26072 lgsquadlem2 27425 oppperpex 28761 outpasch 28763 ushgredgedg 29246 ushgredgedgloop 29248 cusgrfilem2 29474 nsgqusf1olem2 33442 ssmxidl 33502 cmppcmp 33857 eulerpartlemgvv 34378 eulerpartlemgh 34380 fnrelpredd 35103 erdszelem7 35202 rellysconn 35256 ivthALT 36336 fnessref 36358 phpreu 37611 poimirlem26 37653 itg2gt0cn 37682 frinfm 37742 sstotbnd2 37781 heiborlem3 37820 isdrngo3 37966 dihjat1lem 41430 dvh1dim 41444 dochsatshp 41453 mapdpglem2 41675 prjspreln0 42619 pellexlem5 42844 pell14qrss1234 42867 pell1qrss14 42879 lnr2i 43128 hbtlem6 43141 dflim5 43342 tfsconcatrn 43355 naddgeoa 43407 mnuop3d 44290 fvelsetpreimafv 47374 opnneir 48804 |
| Copyright terms: Public domain | W3C validator |