![]() |
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 3788 | . 2 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 → 𝐴 ∈ V) | |
2 | elex 3493 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | dfsbcq2 3781 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑥 ∈ 𝐵)) | |
4 | eleq1 2822 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
5 | clelsb1 2861 | . . 3 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵) | |
6 | 3, 4, 5 | vtoclbg 3560 | . 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) |
7 | 1, 2, 6 | pm5.21nii 380 | 1 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 [wsb 2068 ∈ wcel 2107 Vcvv 3475 [wsbc 3778 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-sbc 3779 |
This theorem is referenced by: tfinds2 7853 filuni 23389 gropeld 28293 grstructeld 28294 f1od2 31946 esum2dlem 33090 bnj110 33869 f1omptsnlem 36217 relowlpssretop 36245 rdgeqoa 36251 minregex 42285 cotrclrcl 42493 frege70 42684 frege72 42686 frege91 42705 sbcoreleleq 43296 onfrALTlem4 43304 sbcoreleleqVD 43620 onfrALTlem4VD 43647 |
Copyright terms: Public domain | W3C validator |