![]() |
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 2093 | . 2 ⊢ 𝐵 = 𝐴 |
3 | eqeltrr.2 | . 2 ⊢ 𝐴 ∈ 𝐶 | |
4 | 2, 3 | eqeltri 2161 | 1 ⊢ 𝐵 ∈ 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1290 ∈ wcel 1439 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-4 1446 ax-17 1465 ax-ial 1473 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-cleq 2082 df-clel 2085 |
This theorem is referenced by: 3eltr3i 2169 p0ex 4029 epse 4178 unex 4276 ordtri2orexmid 4352 onsucsssucexmid 4356 ordsoexmid 4391 ordtri2or2exmid 4400 nnregexmid 4447 abrexex 5902 opabex3 5907 abrexex2 5909 abexssex 5910 abexex 5911 oprabrexex2 5915 tfr0dm 6101 1lt2pi 6953 prarloclemarch2 7032 prarloclemlt 7106 0cn 7534 resubcli 7799 0reALT 7833 10nn 8946 numsucc 8970 nummac 8975 qreccl 9181 unirnioo 9445 sn0topon 11842 bj-unex 12076 exmidsbthrlem 12178 |
Copyright terms: Public domain | W3C validator |