| 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 2377. (Revised by Wolf Lammen, 30-Apr-2023.) |
| Ref | Expression |
|---|---|
| sbcel1v | ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbcex 3798 | . 2 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 → 𝐴 ∈ V) | |
| 2 | elex 3501 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
| 3 | dfsbcq2 3791 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑥 ∈ 𝐵)) | |
| 4 | eleq1 2829 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
| 5 | clelsb1 2868 | . . 3 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵) | |
| 6 | 3, 4, 5 | vtoclbg 3557 | . 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) |
| 7 | 1, 2, 6 | pm5.21nii 378 | 1 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 [wsb 2064 ∈ wcel 2108 Vcvv 3480 [wsbc 3788 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-sbc 3789 |
| This theorem is referenced by: tfinds2 7885 filuni 23893 gropeld 29050 grstructeld 29051 f1od2 32732 esum2dlem 34093 bnj110 34872 f1omptsnlem 37337 relowlpssretop 37365 rdgeqoa 37371 minregex 43547 cotrclrcl 43755 frege70 43946 frege72 43948 frege91 43967 sbcoreleleq 44555 onfrALTlem4 44563 sbcoreleleqVD 44879 onfrALTlem4VD 44906 rspesbcd 44958 |
| Copyright terms: Public domain | W3C validator |