![]() |
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 1912 | . 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))) |
3 | df-rex 3065 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
4 | df-rex 3065 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)) | |
5 | 2, 3, 4 | 3imtr4g 296 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∃wex 1773 ∈ wcel 2098 ∃wrex 3064 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 |
This theorem depends on definitions: df-bi 206 df-ex 1774 df-rex 3065 |
This theorem is referenced by: reximdvai 3159 reximssdv 3166 ssrexv 4046 ssimaex 6970 nnsuc 7870 oaass 8562 omeulem1 8583 ssnnfi 9171 ssnnfiOLD 9172 findcard3 9287 findcard3OLD 9288 unfilem1 9312 epfrs 9728 alephval3 10107 isfin7-2 10393 fpwwe2lem12 10639 inawinalem 10686 ico0 13376 ioc0 13377 r19.2uz 15304 climrlim2 15497 prmdvdsncoprmbd 16672 iserodd 16777 ramub2 16956 prmgaplem6 16998 ablfaclem3 20009 unitgrp 20285 restnlly 23341 llyrest 23344 nllyrest 23345 llyidm 23347 nllyidm 23348 cnpflfi 23858 cnextcn 23926 ivthlem3 25337 dvfsumrlim 25921 lgsquadlem2 27269 oppperpex 28512 outpasch 28514 ushgredgedg 28994 ushgredgedgloop 28996 cusgrfilem2 29222 nsgqusf1olem2 33031 ghmquskerlem2 33036 ssmxidl 33096 cmppcmp 33368 eulerpartlemgvv 33905 eulerpartlemgh 33907 fnrelpredd 34621 erdszelem7 34716 rellysconn 34770 ivthALT 35728 fnessref 35750 phpreu 36985 poimirlem26 37027 itg2gt0cn 37056 frinfm 37116 sstotbnd2 37155 heiborlem3 37194 isdrngo3 37340 dihjat1lem 40812 dvh1dim 40826 dochsatshp 40835 mapdpglem2 41057 prjspreln0 41929 pellexlem5 42149 pell14qrss1234 42172 pell1qrss14 42184 lnr2i 42436 hbtlem6 42449 dflim5 42655 tfsconcatrn 42668 naddgeoa 42721 mnuop3d 43606 fvelsetpreimafv 46627 opnneir 47813 |
Copyright terms: Public domain | W3C validator |