![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfeqd | Structured version Visualization version GIF version |
Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfeqd.1 | ⊢ (𝜑 → Ⅎ𝑥𝐴) |
nfeqd.2 | ⊢ (𝜑 → Ⅎ𝑥𝐵) |
Ref | Expression |
---|---|
nfeqd | ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfcleq 2727 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) | |
2 | nfv 1911 | . . 3 ⊢ Ⅎ𝑦𝜑 | |
3 | nfeqd.1 | . . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝐴) | |
4 | df-nfc 2889 | . . . . . 6 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | |
5 | 3, 4 | sylib 218 | . . . . 5 ⊢ (𝜑 → ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) |
6 | 5 | 19.21bi 2186 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) |
7 | nfeqd.2 | . . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝐵) | |
8 | df-nfc 2889 | . . . . . 6 ⊢ (Ⅎ𝑥𝐵 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐵) | |
9 | 7, 8 | sylib 218 | . . . . 5 ⊢ (𝜑 → ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐵) |
10 | 9 | 19.21bi 2186 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵) |
11 | 6, 10 | nfbid 1899 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) |
12 | 2, 11 | nfald 2326 | . 2 ⊢ (𝜑 → Ⅎ𝑥∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) |
13 | 1, 12 | nfxfrd 1850 | 1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∀wal 1534 = wceq 1536 Ⅎwnf 1779 ∈ wcel 2105 Ⅎwnfc 2887 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1776 df-nf 1780 df-cleq 2726 df-nfc 2889 |
This theorem is referenced by: nfeld 2914 nfeq 2916 nfned 3041 cbvexeqsetf 3492 sbcralt 3880 csbiebt 3937 csbie2df 4448 dfnfc2 4933 eusvnfb 5398 eusv2i 5399 dfid3 5585 iota2df 6549 riotaeqimp 7413 riota5f 7415 oprabid 7462 axrepndlem1 10629 axrepndlem2 10630 axunnd 10633 axpowndlem4 10637 axregndlem2 10640 axinfndlem1 10642 axinfnd 10643 axacndlem4 10647 axacndlem5 10648 axacnd 10649 bj-elgab 36921 bj-gabima 36922 wl-issetft 37562 riotasv2d 38938 nfxnegd 45390 |
Copyright terms: Public domain | W3C validator |