Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfeq | GIF version |
Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfnfc.1 | ⊢ Ⅎ𝑥𝐴 |
nfeq.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfeq | ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfcleq 2131 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑧(𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵)) | |
2 | nfnfc.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2273 | . . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴 |
4 | nfeq.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
5 | 4 | nfcri 2273 | . . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐵 |
6 | 3, 5 | nfbi 1568 | . . 3 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵) |
7 | 6 | nfal 1555 | . 2 ⊢ Ⅎ𝑥∀𝑧(𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵) |
8 | 1, 7 | nfxfr 1450 | 1 ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∀wal 1329 = wceq 1331 Ⅎwnf 1436 ∈ wcel 1480 Ⅎwnfc 2266 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-cleq 2130 df-clel 2133 df-nfc 2268 |
This theorem is referenced by: nfel 2288 nfeq1 2289 nfeq2 2291 nfne 2399 raleqf 2620 rexeqf 2621 reueq1f 2622 rmoeq1f 2623 rabeqf 2671 sbceqg 3013 csbhypf 3033 nfiotadw 5086 nffn 5214 nffo 5339 fvmptdf 5501 mpteqb 5504 fvmptf 5506 eqfnfv2f 5515 dff13f 5664 ovmpos 5887 ov2gf 5888 ovmpodxf 5889 ovmpodf 5895 eqerlem 6453 sumeq2 11121 fsumadd 11168 prodeq1f 11314 prodeq2 11319 txcnp 12429 cnmpt11 12441 cnmpt21 12449 cnmptcom 12456 |
Copyright terms: Public domain | W3C validator |