![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eleq2s | Unicode version |
Description: Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
eleq2s.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
eleq2s.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eleq2s |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2s.2 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | eleq2i 2101 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | eleq2s.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylbi 114 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 df-clel 2033 |
This theorem is referenced by: elrabi 2689 opelopabsb 3988 epelg 4018 elxpi 4304 optocl 4359 fvmptss2 5190 fvmptssdm 5198 acexmidlemcase 5450 elmpt2cl 5640 mpt2xopn0yelv 5795 tfr2a 5877 2oconcl 5961 ecexr 6047 ectocld 6108 ecoptocl 6129 eroveu 6133 dmaddpqlem 6361 nqpi 6362 nq0nn 6425 0nsr 6677 axaddcl 6750 axmulcl 6752 peano2uzs 8303 fzossnn0 8801 frecfzennn 8884 |
Copyright terms: Public domain | W3C validator |