![]() |
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 3835 | . 2 ⊢ (⊤ → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) |
4 | 3 | mptru 1541 | 1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ⊤wtru 1535 [wsbc 3775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-sbc 3776 |
This theorem is referenced by: eqsbc2 3844 sbc3an 3845 sbccomlem 3862 sbccom 3863 sbcrext 3865 sbcabel 3870 csbcow 3906 csbco 3907 sbcnel12g 4408 sbcne12 4409 csbcom 4414 csbnestgfw 4416 csbnestgf 4421 sbccsb 4430 sbccsb2 4431 csbab 4434 2nreu 4438 sbcssg 4518 sbcop 5485 sbcrel 5776 difopabOLD 5827 sbcfung 6572 tfinds2 7863 frpoins3xpg 8143 frpoins3xp3g 8144 mpoxopovel 8224 f1od2 32632 bnj62 34575 bnj89 34576 bnj156 34583 bnj524 34592 bnj610 34602 bnj919 34622 bnj976 34632 bnj110 34713 bnj91 34716 bnj92 34717 bnj106 34723 bnj121 34725 bnj124 34726 bnj125 34727 bnj126 34728 bnj130 34729 bnj154 34733 bnj155 34734 bnj153 34735 bnj207 34736 bnj523 34742 bnj526 34743 bnj539 34746 bnj540 34747 bnj581 34763 bnj591 34766 bnj609 34772 bnj611 34773 bnj934 34790 bnj1000 34796 bnj984 34807 bnj985v 34808 bnj985 34809 bnj1040 34827 bnj1123 34841 bnj1452 34907 bnj1463 34910 sbcalf 37825 sbcexf 37826 sbccom2lem 37835 sbccom2 37836 sbccom2f 37837 sbccom2fi 37838 csbcom2fi 37839 rspcsbnea 41840 2sbcrex 42475 2sbcrexOLD 42477 sbcrot3 42482 sbcrot5 42483 2rexfrabdioph 42487 3rexfrabdioph 42488 4rexfrabdioph 42489 6rexfrabdioph 42490 7rexfrabdioph 42491 rmydioph 42706 expdiophlem2 42714 sbcheg 43480 sbc3or 44242 trsbc 44250 onfrALTlem5 44252 eqsbc2VD 44550 sbcoreleleqVD 44569 onfrALTlem5VD 44595 ich2exprop 47076 |
Copyright terms: Public domain | W3C validator |