![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqeltrri | GIF version |
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqeltrr.1 | ⊢ 𝐴 = 𝐵 |
eqeltrr.2 | ⊢ 𝐴 ∈ 𝐶 |
Ref | Expression |
---|---|
eqeltrri | ⊢ 𝐵 ∈ 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeltrr.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
2 | 1 | eqcomi 2193 | . 2 ⊢ 𝐵 = 𝐴 |
3 | eqeltrr.2 | . 2 ⊢ 𝐴 ∈ 𝐶 | |
4 | 2, 3 | eqeltri 2262 | 1 ⊢ 𝐵 ∈ 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1364 ∈ wcel 2160 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-17 1537 ax-ial 1545 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 df-clel 2185 |
This theorem is referenced by: 3eltr3i 2270 p0ex 4206 epse 4360 unex 4459 ordtri2orexmid 4540 onsucsssucexmid 4544 ordsoexmid 4579 ordtri2or2exmid 4588 ontri2orexmidim 4589 nnregexmid 4638 abrexex 6142 opabex3 6147 abrexex2 6149 abexssex 6150 abexex 6151 oprabrexex2 6155 tfr0dm 6347 exmidonfinlem 7222 1lt2pi 7369 prarloclemarch2 7448 prarloclemlt 7522 0cn 7979 resubcli 8250 0reALT 8284 10nn 9429 numsucc 9453 nummac 9458 qreccl 9672 unirnioo 10003 fz0to4untppr 10154 4sqlem19 12441 prdsex 12774 fn0g 12851 sn0topon 14048 retopbas 14483 blssioo 14505 lgslem4 14865 bj-unex 15132 exmidsbthrlem 15232 |
Copyright terms: Public domain | W3C validator |