![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqeq1 | GIF version |
Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqeq1 | ⊢ (A = B → (A = 𝐶 ↔ B = 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfcleq 2031 | . . . . . 6 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B)) | |
2 | 1 | biimpi 113 | . . . . 5 ⊢ (A = B → ∀x(x ∈ A ↔ x ∈ B)) |
3 | 2 | 19.21bi 1447 | . . . 4 ⊢ (A = B → (x ∈ A ↔ x ∈ B)) |
4 | 3 | bibi1d 222 | . . 3 ⊢ (A = B → ((x ∈ A ↔ x ∈ 𝐶) ↔ (x ∈ B ↔ x ∈ 𝐶))) |
5 | 4 | albidv 1702 | . 2 ⊢ (A = B → (∀x(x ∈ A ↔ x ∈ 𝐶) ↔ ∀x(x ∈ B ↔ x ∈ 𝐶))) |
6 | dfcleq 2031 | . 2 ⊢ (A = 𝐶 ↔ ∀x(x ∈ A ↔ x ∈ 𝐶)) | |
7 | dfcleq 2031 | . 2 ⊢ (B = 𝐶 ↔ ∀x(x ∈ B ↔ x ∈ 𝐶)) | |
8 | 5, 6, 7 | 3bitr4g 212 | 1 ⊢ (A = B → (A = 𝐶 ↔ B = 𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 ∀wal 1240 = wceq 1242 ∈ wcel 1390 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-4 1397 ax-17 1416 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 |
This theorem is referenced by: eqeq1i 2044 eqeq1d 2045 eqeq2 2046 eqeq12 2049 eqtr 2054 eqsb3lem 2137 clelab 2159 neeq1 2213 pm13.18 2280 issetf 2556 sbhypf 2597 vtoclgft 2598 eqvincf 2663 pm13.183 2675 eueq 2706 mob 2717 euind 2722 reuind 2738 eqsbc3 2796 csbhypf 2879 uniiunlem 3022 snjust 3372 elprg 3384 elsncg 3389 rabrsndc 3429 sneqrg 3524 preq12bg 3535 intab 3635 dfiin2g 3681 opthg 3966 copsexg 3972 euotd 3982 elopab 3986 snnex 4147 uniuni 4149 eusv1 4150 reusv3 4158 ordtriexmid 4210 onsucelsucexmidlem1 4213 onsucelsucexmid 4215 regexmidlemm 4217 regexmidlem1 4218 nn0suc 4270 nndceq0 4282 0elnn 4283 elxpi 4304 opbrop 4362 relop 4429 ideqg 4430 elrnmpt 4526 elrnmpt1 4528 elrnmptg 4529 cnveqb 4719 relcoi1 4792 funopg 4877 funcnvuni 4911 fun11iun 5090 fvelrnb 5164 fvmptg 5191 fndmin 5217 eldmrexrn 5251 foelrn 5260 foco2 5261 fmptco 5273 elabrex 5340 abrexco 5341 f1veqaeq 5351 f1oiso 5408 eusvobj2 5441 acexmidlema 5446 acexmidlemb 5447 acexmidlem2 5452 acexmidlemv 5453 oprabid 5480 mpt2fun 5545 elrnmpt2g 5555 elrnmpt2 5556 ralrnmpt2 5557 rexrnmpt2 5558 ovi3 5579 ov6g 5580 ovelrn 5591 caovcang 5604 caovcan 5607 eloprabi 5764 dftpos4 5819 elqsg 6092 qsel 6119 brecop 6132 eroveu 6133 erovlem 6134 th3qlem1 6144 th3q 6147 2dom 6221 fundmen 6222 indpi 6326 nqtri3or 6380 enq0sym 6415 enq0ref 6416 enq0tr 6417 enq0breq 6419 addnq0mo 6430 mulnq0mo 6431 mulnnnq0 6433 genipv 6492 genpelvl 6495 genpelvu 6496 addsrmo 6671 mulsrmo 6672 aptisr 6705 ltresr 6736 axcnre 6765 axpre-apti 6769 apreap 7371 apreim 7387 creur 7692 creui 7693 nn1m1nn 7713 nn1gt1 7728 elz 8023 nn0ind-raph 8131 nltpnft 8500 xnegeq 8510 expival 8911 bj-nn0suc0 9410 bj-inf2vnlem1 9430 bj-inf2vnlem2 9431 bj-nn0sucALT 9438 |
Copyright terms: Public domain | W3C validator |