Theorem sbcieg 3786

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.) Avoid ax-10 2178, ax-12 2215. (Revised by GG, 12-Oct-2024.)

Hypothesis

Ref	Expression
sbcieg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
sbcieg	⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem sbcieg

Step	Hyp	Ref	Expression
1		df-sbc 3748	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
2		sbcieg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	elabg 3638	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	1, 3	bitrid 286	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ∈ wcel 2145  {cab 2743  [wsbc 3747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-sbc 3748

This theorem is referenced by:  sbcie  3788  2nreu  4401  reuprg0  4664  rabsnif  4685  ralrnmptw  7079  ralrnmpt  7081  fpwwe2lem3  10606  nn1suc  12243  opfi1uzind  14536  mndind  18875  fgcl  23992  cfinfil  24007  csdfil  24008  supfil  24009  fin1aufil  24046  ifeqeqx  32794  nn0min  33073  bnj1452  35352  cdlemk35s  41568  cdlemk39s  41570  cdlemk42  41572  2nn0ind  43529  zindbi  43530  prproropreud  48114