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 2231 | . 2 |
3 | eleq2s.1 | . 2 | |
4 | 2, 3 | sylbi 120 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1342 wcel 2135 |
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 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-4 1497 ax-17 1513 ax-ial 1521 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 df-clel 2160 |
This theorem is referenced by: elrabi 2875 opelopabsb 4233 epelg 4263 reg3exmidlemwe 4551 elxpi 4615 optocl 4675 fvmptss2 5556 fvmptssdm 5565 acexmidlemcase 5832 elmpocl 6031 mpoxopn0yelv 6199 tfr2a 6281 tfri1dALT 6311 2oconcl 6399 el2oss1o 6403 ecexr 6498 ectocld 6559 ecoptocl 6580 eroveu 6584 mapsnconst 6652 diffitest 6845 en2eqpr 6865 ctssdccl 7068 exmidonfinlem 7141 exmidfodomrlemr 7150 exmidfodomrlemrALT 7151 dmaddpqlem 7310 nqpi 7311 nq0nn 7375 0nsr 7682 suplocsrlempr 7740 cnm 7765 axaddcl 7797 axmulcl 7799 aprcl 8536 peano2uzs 9514 fzssnn 9994 fzossnn0 10101 rebtwn2zlemstep 10179 fldiv4p1lem1div2 10231 frecfzennn 10352 fser0const 10442 facnn 10630 bcpasc 10669 hashfzo0 10726 rexuz3 10922 rexanuz2 10923 r19.2uz 10925 cau4 11048 caubnd2 11049 climshft2 11237 climaddc1 11260 climmulc2 11262 climsubc1 11263 climsubc2 11264 climlec2 11272 climcau 11278 climcaucn 11282 iserabs 11406 binomlem 11414 isumshft 11421 cvgratgt0 11464 clim2divap 11471 ntrivcvgap 11479 fprodntrivap 11515 fprodeq0 11548 infssuzex 11871 infssuzledc 11872 3prm 12049 phicl2 12135 phibndlem 12137 dfphi2 12141 crth 12145 phimullem 12146 znnen 12294 ennnfonelemkh 12308 bj-el2oss1o 13517 2o01f 13738 nninfalllem1 13750 nninfall 13751 |
Copyright terms: Public domain | W3C validator |