| 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 2729 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) | |
| 2 | nfv 1915 | . . 3 ⊢ Ⅎ𝑦𝜑 | |
| 3 | nfeqd.1 | . . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝐴) | |
| 4 | df-nfc 2885 | . . . . . 6 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | |
| 5 | 3, 4 | sylib 218 | . . . . 5 ⊢ (𝜑 → ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) |
| 6 | 5 | 19.21bi 2196 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) |
| 7 | nfeqd.2 | . . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝐵) | |
| 8 | df-nfc 2885 | . . . . . 6 ⊢ (Ⅎ𝑥𝐵 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐵) | |
| 9 | 7, 8 | sylib 218 | . . . . 5 ⊢ (𝜑 → ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐵) |
| 10 | 9 | 19.21bi 2196 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵) |
| 11 | 6, 10 | nfbid 1903 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) |
| 12 | 2, 11 | nfald 2333 | . 2 ⊢ (𝜑 → Ⅎ𝑥∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) |
| 13 | 1, 12 | nfxfrd 1855 | 1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1539 = wceq 1541 Ⅎwnf 1784 ∈ wcel 2113 Ⅎwnfc 2883 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1781 df-nf 1785 df-cleq 2728 df-nfc 2885 |
| This theorem is referenced by: nfeld 2910 nfeq 2912 nfned 3034 cbvexeqsetf 3455 sbcralt 3822 csbiebt 3878 csbie2df 4395 dfnfc2 4885 eusvnfb 5338 eusv2i 5339 dfid3 5522 iota2df 6479 riotaeqimp 7341 riota5f 7343 oprabid 7390 axrepndlem1 10505 axrepndlem2 10506 axunnd 10509 axpowndlem4 10513 axregndlem2 10516 axinfndlem1 10518 axinfnd 10519 axacndlem4 10523 axacndlem5 10524 axacnd 10525 bj-elgab 37142 bj-gabima 37143 wl-issetft 37789 riotasv2d 39239 nfxnegd 45706 |
| Copyright terms: Public domain | W3C validator |