![]() |
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 3785 | . 2 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 → 𝐴 ∈ V) | |
2 | elex 3493 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | dfsbcq2 3778 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑥 ∈ 𝐵)) | |
4 | eleq1 2822 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
5 | clelsb1 2861 | . . 3 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵) | |
6 | 3, 4, 5 | vtoclbg 3558 | . 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 3775 |
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 3776 |
This theorem is referenced by: tfinds2 7847 filuni 23370 gropeld 28272 grstructeld 28273 f1od2 31923 esum2dlem 33027 bnj110 33806 f1omptsnlem 36154 relowlpssretop 36182 rdgeqoa 36188 minregex 42217 cotrclrcl 42425 frege70 42616 frege72 42618 frege91 42637 sbcoreleleq 43228 onfrALTlem4 43236 sbcoreleleqVD 43552 onfrALTlem4VD 43579 |
Copyright terms: Public domain | W3C validator |