![]() |
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 2871 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
2 | nfv 1915 | . . 3 ⊢ Ⅎ𝑦𝜑 | |
3 | nfcvd 2956 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝑦) | |
4 | nfeqd.1 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴) | |
5 | 3, 4 | nfeqd 2965 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 = 𝐴) |
6 | nfeqd.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐵) | |
7 | 6 | nfcrd 2945 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵) |
8 | 5, 7 | nfand 1898 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵)) |
9 | 2, 8 | nfexd 2337 | . 2 ⊢ (𝜑 → Ⅎ𝑥∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵)) |
10 | 1, 9 | nfxfrd 1855 | 1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 ∃wex 1781 Ⅎwnf 1785 ∈ wcel 2111 Ⅎwnfc 2936 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-nf 1786 df-cleq 2791 df-clel 2870 df-nfc 2938 |
This theorem is referenced by: nfel 2969 nfneld 3099 nfraldw 3187 nfrald 3188 ralcom2 3316 nfreud 3325 nfrmod 3326 nfreuw 3327 nfrmow 3328 nfrmo 3330 nfsbc1d 3738 nfsbcdw 3741 nfsbcd 3744 sbcrext 3802 nfdisjw 5007 nfdisj 5008 nfbrd 5076 nfriotadw 7101 nfriotad 7104 nfixpw 8463 nfixp 8464 axrepndlem2 10004 axrepnd 10005 axunnd 10007 axpowndlem2 10009 axpowndlem3 10010 axpowndlem4 10011 axpownd 10012 axregndlem2 10014 axinfndlem1 10016 axinfnd 10017 axacndlem4 10021 axacndlem5 10022 axacnd 10023 |
Copyright terms: Public domain | W3C validator |