![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqsstri | GIF version |
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.) |
Ref | Expression |
---|---|
eqsstr.1 | ⊢ 𝐴 = 𝐵 |
eqsstr.2 | ⊢ 𝐵 ⊆ 𝐶 |
Ref | Expression |
---|---|
eqsstri | ⊢ 𝐴 ⊆ 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqsstr.2 | . 2 ⊢ 𝐵 ⊆ 𝐶 | |
2 | eqsstr.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
3 | 2 | sseq1i 3128 | . 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) |
4 | 1, 3 | mpbir 145 | 1 ⊢ 𝐴 ⊆ 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1332 ⊆ wss 3076 |
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-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-11 1485 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-in 3082 df-ss 3089 |
This theorem is referenced by: eqsstrri 3135 ssrab2 3187 rabssab 3189 difdifdirss 3452 opabss 4000 brab2ga 4622 relopabi 4673 dmopabss 4759 resss 4851 relres 4855 exse2 4921 rnin 4956 rnxpss 4978 cnvcnvss 5001 dmmptss 5043 cocnvss 5072 fnres 5247 resasplitss 5310 fabexg 5318 f0 5321 ffvresb 5591 isoini2 5728 dmoprabss 5861 elmpocl 5976 tposssxp 6154 dftpos4 6168 smores 6197 smores2 6199 iordsmo 6202 swoer 6465 swoord1 6466 swoord2 6467 ecss 6478 ecopovsym 6533 ecopovtrn 6534 ecopover 6535 ecopovsymg 6536 ecopovtrng 6537 ecopoverg 6538 sbthlem7 6859 caserel 6980 ctssdccl 7004 pinn 7141 niex 7144 ltrelpi 7156 dmaddpi 7157 dmmulpi 7158 enqex 7192 ltrelnq 7197 enq0ex 7271 ltrelpr 7337 enrex 7569 ltrelsr 7570 ltrelre 7665 axaddf 7700 axmulf 7701 ltrelxr 7849 lerelxr 7851 nn0ssre 9005 nn0ssz 9096 rpre 9477 fz1ssfz0 9928 cau3 10919 fsum3cvg3 11197 isumshft 11291 explecnv 11306 clim2prod 11340 ntrivcvgap 11349 dvdszrcl 11534 dvdsflip 11585 infssuzcldc 11680 phimullem 11937 ctiunctlemuom 11985 structcnvcnv 12014 fvsetsid 12032 strleun 12087 dmtopon 12229 lmfval 12400 lmbrf 12423 cnconst2 12441 txuni2 12464 xmeter 12644 ivthinclemex 12828 dvrecap 12885 |
Copyright terms: Public domain | W3C validator |