| 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 3448), 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 3448 | . 2 ⊢ 𝑥 ∈ V | |
| 2 | vex 3448 | . 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 2109 Vcvv 3444 |
| 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 2008 ax-8 2111 ax-9 2119 ax-ext 2701 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-v 3446 |
| This theorem is referenced by: codir 6081 dfco2 6206 1st2val 7975 2nd2val 7976 fnmap 8783 enrefnn 8995 unfi 9112 wemappo 9478 wemapsolem 9479 fin23lem26 10254 seqval 13953 hash2exprb 14412 hashle2prv 14419 hash3tpexb 14435 mreexexlem4d 17588 pmtrrn2 19374 c0snmgmhm 20382 alexsubALTlem4 23970 elqaalem2 26261 seqsval 28222 upgrex 29072 cusgrsize 29435 erclwwlkref 29999 erclwwlksym 30000 erclwwlknref 30048 erclwwlknsym 30049 eclclwwlkn1 30054 gonanegoal 35332 gonarlem 35374 gonar 35375 fmla0disjsuc 35378 fmlasucdisj 35379 mclsppslem 35563 fneer 36334 curunc 37589 matunitlindflem2 37604 vvdifopab 38242 inxprnres 38273 ineccnvmo 38332 alrmomorn 38333 dfcoss2 38397 dfcoss3 38398 cosscnv 38400 cocossss 38420 cnvcosseq 38421 refressn 38427 antisymressn 38428 trressn 38429 rncossdmcoss 38439 symrelcoss3 38449 1cosscnvxrn 38459 cosscnvssid3 38460 cosscnvssid4 38461 coss0 38463 trcoss 38466 trcoss2 38468 erimeq2 38663 dfeldisj3 38704 dfeldisj4 38705 dfantisymrel5 38747 ismrc 42682 en2pr 43529 pr2cv 43530 permaxext 44988 permac8prim 44997 ovnsubaddlem1 46561 sprsymrelfvlem 47484 sprsymrelf1lem 47485 prprelb 47510 prprspr2 47512 reuprpr 47517 2exopprim 47519 reuopreuprim 47520 |
| Copyright terms: Public domain | W3C validator |