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.) |
Ref | Expression |
---|---|
sbcel1v | ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcex 3412 | . 2 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 → 𝐴 ∈ V) | |
2 | elex 3185 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | dfsbcq2 3405 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑥 ∈ 𝐵)) | |
4 | eleq1 2676 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
5 | clelsb3 2716 | . . 3 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵) | |
6 | 3, 4, 5 | vtoclbg 3240 | . 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) |
7 | 1, 2, 6 | pm5.21nii 367 | 1 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 [wsb 1867 ∈ wcel 1977 Vcvv 3173 [wsbc 3402 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-v 3175 df-sbc 3403 |
This theorem is referenced by: tfinds2 6955 filuni 21499 gropeld 25710 grstructeld 25711 f1od2 28887 esum2dlem 29481 bnj110 30182 f1omptsnlem 32359 relowlpssretop 32388 rdgeqoa 32394 cotrclrcl 37053 frege70 37247 frege72 37249 frege91 37268 sbcoreleleq 37766 onfrALTlem4 37779 |
Copyright terms: Public domain | W3C validator |