| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sbcbii | Structured version Visualization version GIF version | ||
| Description: Formula-building inference for class substitution. (Contributed by NM, 11-Nov-2005.) |
| Ref | Expression |
|---|---|
| sbcbii.1 | ⊢ (𝜑 ↔ 𝜓) |
| Ref | Expression |
|---|---|
| sbcbii | ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbcbii.1 | . . . 4 ⊢ (𝜑 ↔ 𝜓) | |
| 2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓)) |
| 3 | 2 | sbcbidv 3845 | . 2 ⊢ (⊤ → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) |
| 4 | 3 | mptru 1547 | 1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ⊤wtru 1541 [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-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-sbc 3789 |
| This theorem is referenced by: eqsbc2 3854 sbc3an 3855 sbccomlemOLD 3870 sbccom 3871 sbcrext 3873 sbcabel 3878 csbcow 3914 csbco 3915 sbcnel12g 4414 sbcne12 4415 csbcom 4420 csbnestgfw 4422 csbnestgf 4427 sbccsb 4436 sbccsb2 4437 csbab 4440 2nreu 4444 sbcssg 4520 sbcop 5494 sbcrel 5790 difopabOLD 5841 sbcfung 6590 tfinds2 7885 frpoins3xpg 8165 frpoins3xp3g 8166 mpoxopovel 8245 f1od2 32732 bnj62 34734 bnj89 34735 bnj156 34742 bnj524 34751 bnj610 34761 bnj919 34781 bnj976 34791 bnj110 34872 bnj91 34875 bnj92 34876 bnj106 34882 bnj121 34884 bnj124 34885 bnj125 34886 bnj126 34887 bnj130 34888 bnj154 34892 bnj155 34893 bnj153 34894 bnj207 34895 bnj523 34901 bnj526 34902 bnj539 34905 bnj540 34906 bnj581 34922 bnj591 34925 bnj609 34931 bnj611 34932 bnj934 34949 bnj1000 34955 bnj984 34966 bnj985v 34967 bnj985 34968 bnj1040 34986 bnj1123 35000 bnj1452 35066 bnj1463 35069 sbcalf 38121 sbcexf 38122 sbccom2lem 38131 sbccom2 38132 sbccom2f 38133 sbccom2fi 38134 csbcom2fi 38135 rspcsbnea 42132 2sbcrex 42795 2sbcrexOLD 42797 sbcrot3 42802 sbcrot5 42803 2rexfrabdioph 42807 3rexfrabdioph 42808 4rexfrabdioph 42809 6rexfrabdioph 42810 7rexfrabdioph 42811 rmydioph 43026 expdiophlem2 43034 sbcheg 43792 sbc3or 44552 trsbc 44560 onfrALTlem5 44562 eqsbc2VD 44860 sbcoreleleqVD 44879 onfrALTlem5VD 44905 ich2exprop 47458 |
| Copyright terms: Public domain | W3C validator |