![]() |
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 2207 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | eleq2s.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylbi 120 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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-5 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 df-clel 2136 |
This theorem is referenced by: elrabi 2841 opelopabsb 4190 epelg 4220 reg3exmidlemwe 4501 elxpi 4563 optocl 4623 fvmptss2 5504 fvmptssdm 5513 acexmidlemcase 5777 elmpocl 5976 mpoxopn0yelv 6144 tfr2a 6226 tfri1dALT 6256 2oconcl 6344 ecexr 6442 ectocld 6503 ecoptocl 6524 eroveu 6528 mapsnconst 6596 diffitest 6789 en2eqpr 6809 ctssdccl 7004 exmidonfinlem 7066 exmidfodomrlemr 7075 exmidfodomrlemrALT 7076 dmaddpqlem 7209 nqpi 7210 nq0nn 7274 0nsr 7581 suplocsrlempr 7639 cnm 7664 axaddcl 7696 axmulcl 7698 aprcl 8432 peano2uzs 9406 fzssnn 9879 fzossnn0 9983 rebtwn2zlemstep 10061 fldiv4p1lem1div2 10109 frecfzennn 10230 fser0const 10320 facnn 10505 bcpasc 10544 hashfzo0 10601 rexuz3 10794 rexanuz2 10795 r19.2uz 10797 cau4 10920 caubnd2 10921 climshft2 11107 climaddc1 11130 climmulc2 11132 climsubc1 11133 climsubc2 11134 climlec2 11142 climcau 11148 climcaucn 11152 iserabs 11276 binomlem 11284 isumshft 11291 cvgratgt0 11334 clim2divap 11341 ntrivcvgap 11349 infssuzex 11678 infssuzledc 11679 3prm 11845 phicl2 11926 phibndlem 11928 dfphi2 11932 crth 11936 phimullem 11937 znnen 11947 ennnfonelemkh 11961 bj-el2oss1o 13152 el2oss1o 13359 2o01f 13364 nninfalllem1 13378 nninfall 13379 |
Copyright terms: Public domain | W3C validator |