![]() |
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 2730 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) | |
2 | nfv 1917 | . . 3 ⊢ Ⅎ𝑦𝜑 | |
3 | nfeqd.1 | . . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝐴) | |
4 | df-nfc 2887 | . . . . . 6 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | |
5 | 3, 4 | sylib 217 | . . . . 5 ⊢ (𝜑 → ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) |
6 | 5 | 19.21bi 2182 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) |
7 | nfeqd.2 | . . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝐵) | |
8 | df-nfc 2887 | . . . . . 6 ⊢ (Ⅎ𝑥𝐵 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐵) | |
9 | 7, 8 | sylib 217 | . . . . 5 ⊢ (𝜑 → ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐵) |
10 | 9 | 19.21bi 2182 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵) |
11 | 6, 10 | nfbid 1905 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) |
12 | 2, 11 | nfald 2322 | . 2 ⊢ (𝜑 → Ⅎ𝑥∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) |
13 | 1, 12 | nfxfrd 1856 | 1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1539 = wceq 1541 Ⅎ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-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-ex 1782 df-nf 1786 df-cleq 2729 df-nfc 2887 |
This theorem is referenced by: nfeld 2916 nfeq 2918 nfned 3044 vtoclgft 3507 sbcralt 3826 csbiebt 3883 csbie2df 4398 dfnfc2 4888 eusvnfb 5346 eusv2i 5347 dfid3 5532 iota2df 6480 riotaeqimp 7334 riota5f 7336 oprabid 7383 axrepndlem1 10486 axrepndlem2 10487 axunnd 10490 axpowndlem4 10494 axregndlem2 10497 axinfndlem1 10499 axinfnd 10500 axacndlem4 10504 axacndlem5 10505 axacnd 10506 bj-elgab 35347 bj-gabima 35348 wl-issetft 35972 riotasv2d 37357 nfxnegd 43581 |
Copyright terms: Public domain | W3C validator |