| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sbceq1a | Structured version Visualization version GIF version | ||
| Description: Equality theorem for class substitution. Class version of sbequ12 2251. (Contributed by NM, 26-Sep-2003.) |
| Ref | Expression |
|---|---|
| sbceq1a | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbid 2255 | . 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑) | |
| 2 | dfsbcq2 3791 | . 2 ⊢ (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
| 3 | 1, 2 | bitr3id 285 | 1 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 [wsb 2064 [wsbc 3788 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-sbc 3789 |
| This theorem is referenced by: sbceq2a 3800 elrabsf 3834 cbvralcsf 3941 reusngf 4674 rexreusng 4679 reuprg0 4702 rmosn 4719 rabsnifsb 4722 euotd 5518 reuop 6313 frpoinsg 6364 wfisgOLD 6375 elfvmptrab1w 7043 elfvmptrab1 7044 ralrnmpt 7116 riotass2 7418 riotass 7419 oprabv 7493 elovmporab 7679 elovmporab1w 7680 elovmporab1 7681 ovmpt3rabdm 7692 elovmpt3rab1 7693 tfisg 7875 tfindes 7884 sbcopeq1a 8074 sbcoteq1a 8076 mpoxopoveq 8244 findcard2 9204 ac6sfi 9320 indexfi 9400 frinsg 9791 nn0ind-raph 12718 fzrevral 13652 wrdind 14760 wrd2ind 14761 prmind2 16722 elmptrab 23835 isfildlem 23865 2sqreulem4 27498 gropd 29048 grstructd 29049 rspc2daf 32485 opreu2reuALT 32496 ifeqeqx 32555 wrdt2ind 32938 bnj919 34781 bnj976 34791 bnj1468 34860 bnj110 34872 bnj150 34890 bnj151 34891 bnj607 34930 bnj873 34938 bnj849 34939 bnj1388 35047 setinds 35779 dfon2lem1 35784 rdgssun 37379 indexdom 37741 sdclem2 37749 sdclem1 37750 fdc1 37753 riotasv2s 38959 elimhyps 38962 sbccomieg 42804 rexrabdioph 42805 rexfrabdioph 42806 aomclem6 43071 pm13.13a 44426 pm13.13b 44427 pm13.14 44428 tratrb 44556 uzwo4 45058 or2expropbilem2 47045 reuf1odnf 47119 ich2exprop 47458 ichnreuop 47459 ichreuopeq 47460 prproropreud 47496 reupr 47509 reuopreuprim 47513 |
| Copyright terms: Public domain | W3C validator |