Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbcel1v | Structured version Visualization version GIF version |
Description: Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.) Avoid ax-13 2372. (Revised by Wolf Lammen, 30-Apr-2023.) |
Ref | Expression |
---|---|
sbcel1v | ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcex 3726 | . 2 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 → 𝐴 ∈ V) | |
2 | elex 3450 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | dfsbcq2 3719 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑥 ∈ 𝐵)) | |
4 | eleq1 2826 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
5 | clelsb1 2866 | . . 3 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵) | |
6 | 3, 4, 5 | vtoclbg 3507 | . 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) |
7 | 1, 2, 6 | pm5.21nii 380 | 1 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 [wsb 2067 ∈ wcel 2106 Vcvv 3432 [wsbc 3716 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-sbc 3717 |
This theorem is referenced by: tfinds2 7710 filuni 23036 gropeld 27403 grstructeld 27404 f1od2 31056 esum2dlem 32060 bnj110 32838 f1omptsnlem 35507 relowlpssretop 35535 rdgeqoa 35541 minregex 41141 cotrclrcl 41350 frege70 41541 frege72 41543 frege91 41562 sbcoreleleq 42155 onfrALTlem4 42163 sbcoreleleqVD 42479 onfrALTlem4VD 42506 |
Copyright terms: Public domain | W3C validator |