| 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 1914 | . . 3 ⊢ Ⅎ𝑦𝜑 | |
| 3 | nfeqd.1 | . . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝐴) | |
| 4 | df-nfc 2892 | . . . . . 6 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | |
| 5 | 3, 4 | sylib 218 | . . . . 5 ⊢ (𝜑 → ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) |
| 6 | 5 | 19.21bi 2189 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) |
| 7 | nfeqd.2 | . . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝐵) | |
| 8 | df-nfc 2892 | . . . . . 6 ⊢ (Ⅎ𝑥𝐵 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐵) | |
| 9 | 7, 8 | sylib 218 | . . . . 5 ⊢ (𝜑 → ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐵) |
| 10 | 9 | 19.21bi 2189 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵) |
| 11 | 6, 10 | nfbid 1902 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) |
| 12 | 2, 11 | nfald 2328 | . 2 ⊢ (𝜑 → Ⅎ𝑥∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) |
| 13 | 1, 12 | nfxfrd 1854 | 1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 = wceq 1540 Ⅎwnf 1783 ∈ wcel 2108 Ⅎwnfc 2890 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 df-cleq 2729 df-nfc 2892 |
| This theorem is referenced by: nfeld 2917 nfeq 2919 nfned 3044 cbvexeqsetf 3495 sbcralt 3872 csbiebt 3928 csbie2df 4443 dfnfc2 4929 eusvnfb 5393 eusv2i 5394 dfid3 5581 iota2df 6548 riotaeqimp 7414 riota5f 7416 oprabid 7463 axrepndlem1 10632 axrepndlem2 10633 axunnd 10636 axpowndlem4 10640 axregndlem2 10643 axinfndlem1 10645 axinfnd 10646 axacndlem4 10650 axacndlem5 10651 axacnd 10652 bj-elgab 36940 bj-gabima 36941 wl-issetft 37583 riotasv2d 38958 nfxnegd 45452 |
| Copyright terms: Public domain | W3C validator |