![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfeld | Structured version Visualization version GIF version |
Description: Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfeqd.1 | ⊢ (𝜑 → Ⅎ𝑥𝐴) |
nfeqd.2 | ⊢ (𝜑 → Ⅎ𝑥𝐵) |
Ref | Expression |
---|---|
nfeld | ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfclel 2815 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
2 | nfv 1917 | . . 3 ⊢ Ⅎ𝑦𝜑 | |
3 | nfcvd 2906 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝑦) | |
4 | nfeqd.1 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴) | |
5 | 3, 4 | nfeqd 2915 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 = 𝐴) |
6 | nfeqd.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐵) | |
7 | 6 | nfcrd 2894 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵) |
8 | 5, 7 | nfand 1900 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵)) |
9 | 2, 8 | nfexd 2322 | . 2 ⊢ (𝜑 → Ⅎ𝑥∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵)) |
10 | 1, 9 | nfxfrd 1856 | 1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∃wex 1781 Ⅎwnf 1785 ∈ wcel 2106 Ⅎwnfc 2885 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-ex 1782 df-nf 1786 df-cleq 2728 df-clel 2814 df-nfc 2887 |
This theorem is referenced by: nfel 2919 nfneld 3055 nfraldwOLD 3300 nfrald 3343 ralcom2 3348 nfreuwOLD 3395 nfrmowOLD 3396 nfrmod 3401 nfreud 3402 nfrmo 3403 nfsbc1d 3755 nfsbcdw 3758 nfsbcd 3761 sbcrext 3827 nfdisjw 5080 nfdisj 5081 nfbrd 5149 nfriotadw 7317 nfriotad 7321 nfixpw 8850 nfixp 8851 axrepndlem2 10525 axrepnd 10526 axunnd 10528 axpowndlem2 10530 axpowndlem3 10531 axpowndlem4 10532 axpownd 10533 axregndlem2 10535 axinfndlem1 10537 axinfnd 10538 axacndlem4 10542 axacndlem5 10543 axacnd 10544 |
Copyright terms: Public domain | W3C validator |