Theorem sbcel1v 3838

Description: Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.) Avoid ax-13 2386. (Revised by Wolf Lammen, 30-Apr-2023.)

Assertion

Ref	Expression
sbcel1v	⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)

Distinct variable group:   𝑥,𝐵

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem sbcel1v

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sbcex 3781	. 2 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 → 𝐴 ∈ V)
2		elex 3512	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		dfsbcq2 3774	. . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑥 ∈ 𝐵))
4		eleq1 2900	. . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		clelsb3 2940	. . 3 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)
6	3, 4, 5	vtoclbg 3568	. 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7	1, 2, 6	pm5.21nii 382	1 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)

Syntax hints:   ↔ wb 208  [wsb 2065   ∈ wcel 2110  Vcvv 3494  [wsbc 3771

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3496  df-sbc 3772

This theorem is referenced by:  tfinds2  7572  filuni  22487  gropeld  26812  grstructeld  26813  f1od2  30451  esum2dlem  31346  bnj110  32125  f1omptsnlem  34611  relowlpssretop  34639  rdgeqoa  34645  cotrclrcl  40080  frege70  40272  frege72  40274  frege91  40293  sbcoreleleq  40862  onfrALTlem4  40870  sbcoreleleqVD  41186  onfrALTlem4VD  41213