![]() |
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 2803 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
2 | nfv 1909 | . . 3 ⊢ Ⅎ𝑦𝜑 | |
3 | nfcvd 2892 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝑦) | |
4 | nfeqd.1 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴) | |
5 | 3, 4 | nfeqd 2902 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 = 𝐴) |
6 | nfeqd.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐵) | |
7 | 6 | nfcrd 2884 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵) |
8 | 5, 7 | nfand 1892 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵)) |
9 | 2, 8 | nfexd 2317 | . 2 ⊢ (𝜑 → Ⅎ𝑥∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵)) |
10 | 1, 9 | nfxfrd 1848 | 1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ∃wex 1773 Ⅎwnf 1777 ∈ wcel 2098 Ⅎwnfc 2875 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-ex 1774 df-nf 1778 df-cleq 2717 df-clel 2802 df-nfc 2877 |
This theorem is referenced by: nfel 2906 nfneld 3044 nfraldwOLD 3308 nfrald 3355 ralcom2 3360 nfreuwOLD 3408 nfrmowOLD 3409 nfrmod 3414 nfreud 3415 nfrmo 3416 nfsbc1d 3791 nfsbcdw 3794 nfsbcd 3797 sbcrext 3863 nfdisjw 5126 nfdisj 5127 nfbrd 5195 nfriotadw 7383 nfriotad 7387 nfixpw 8935 nfixp 8936 axrepndlem2 10623 axrepnd 10624 axunnd 10626 axpowndlem2 10628 axpowndlem3 10629 axpowndlem4 10630 axpownd 10631 axregndlem2 10633 axinfndlem1 10635 axinfnd 10636 axacndlem4 10640 axacndlem5 10641 axacnd 10642 |
Copyright terms: Public domain | W3C validator |