| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > el2v | Structured version Visualization version GIF version | ||
| Description: If a proposition is implied by 𝑥 ∈ V and 𝑦 ∈ V (which is true, see vex 3484), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.) |
| Ref | Expression |
|---|---|
| el2v.1 | ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑) |
| Ref | Expression |
|---|---|
| el2v | ⊢ 𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex 3484 | . 2 ⊢ 𝑥 ∈ V | |
| 2 | vex 3484 | . 2 ⊢ 𝑦 ∈ V | |
| 3 | el2v.1 | . 2 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑) | |
| 4 | 1, 2, 3 | mp2an 692 | 1 ⊢ 𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 Vcvv 3480 |
| 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 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 |
| This theorem is referenced by: codir 6140 dfco2 6265 1st2val 8042 2nd2val 8043 fnmap 8873 enrefnn 9087 unfi 9211 wemappo 9589 wemapsolem 9590 fin23lem26 10365 seqval 14053 hash2exprb 14510 hashle2prv 14517 hash3tpexb 14533 mreexexlem4d 17690 pmtrrn2 19478 c0snmgmhm 20462 alexsubALTlem4 24058 elqaalem2 26362 seqsval 28294 upgrex 29109 cusgrsize 29472 erclwwlkref 30039 erclwwlksym 30040 erclwwlknref 30088 erclwwlknsym 30089 eclclwwlkn1 30094 gonanegoal 35357 gonarlem 35399 gonar 35400 fmla0disjsuc 35403 fmlasucdisj 35404 mclsppslem 35588 fneer 36354 curunc 37609 matunitlindflem2 37624 vvdifopab 38261 inxprnres 38293 ineccnvmo 38358 alrmomorn 38359 dfcoss2 38414 dfcoss3 38415 cosscnv 38417 cocossss 38437 cnvcosseq 38438 refressn 38444 antisymressn 38445 trressn 38446 rncossdmcoss 38456 symrelcoss3 38466 1cosscnvxrn 38476 cosscnvssid3 38477 cosscnvssid4 38478 coss0 38480 trcoss 38483 trcoss2 38485 erimeq2 38679 dfeldisj3 38720 dfeldisj4 38721 dfantisymrel5 38763 ismrc 42712 en2pr 43560 pr2cv 43561 ovnsubaddlem1 46585 sprsymrelfvlem 47477 sprsymrelf1lem 47478 prprelb 47503 prprspr2 47505 reuprpr 47510 2exopprim 47512 reuopreuprim 47513 |
| Copyright terms: Public domain | W3C validator |