| 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 17584 pmtrrn2 19366 c0snmgmhm 20347 alexsubALTlem4 23913 elqaalem2 26204 seqsval 28158 upgrex 28995 cusgrsize 29358 erclwwlkref 29922 erclwwlksym 29923 erclwwlknref 29971 erclwwlknsym 29972 eclclwwlkn1 29977 gonanegoal 35312 gonarlem 35354 gonar 35355 fmla0disjsuc 35358 fmlasucdisj 35359 mclsppslem 35543 fneer 36314 curunc 37569 matunitlindflem2 37584 vvdifopab 38222 inxprnres 38253 ineccnvmo 38312 alrmomorn 38313 dfcoss2 38377 dfcoss3 38378 cosscnv 38380 cocossss 38400 cnvcosseq 38401 refressn 38407 antisymressn 38408 trressn 38409 rncossdmcoss 38419 symrelcoss3 38429 1cosscnvxrn 38439 cosscnvssid3 38440 cosscnvssid4 38441 coss0 38443 trcoss 38446 trcoss2 38448 erimeq2 38643 dfeldisj3 38684 dfeldisj4 38685 dfantisymrel5 38727 ismrc 42662 en2pr 43509 pr2cv 43510 permaxext 44968 permac8prim 44977 ovnsubaddlem1 46541 sprsymrelfvlem 47464 sprsymrelf1lem 47465 prprelb 47490 prprspr2 47492 reuprpr 47497 2exopprim 47499 reuopreuprim 47500 |
| Copyright terms: Public domain | W3C validator |