Theorem csbiegf 2021

Description: Conversion of implicit substitution to explicit substitution into a class.

Hypotheses

Ref	Expression
csbiegf.1	⊢ (A ∈ D → (y ∈ C → ∀x y ∈ C))
csbiegf.2	⊢ (x = A → B = C)

Assertion

Ref	Expression
csbiegf	⊢ (A ∈ D → [A / x]B = C)

Distinct variable groups:   x,y,A   y,C   x,D,y

Proof of Theorem csbiegf

Step	Hyp	Ref	Expression
1		csbiegf.1	. . . 4 ⊢ (A ∈ D → (y ∈ C → ∀x y ∈ C))
2	1	19.21aivv 1282	. . 3 ⊢ (A ∈ D → ∀x∀y(y ∈ C → ∀x y ∈ C))
3		csbiegf.2	. . . 4 ⊢ (x = A → B = C)
4	3	ax-gen 960	. . 3 ⊢ ∀x(x = A → B = C)
5	2, 4	jctir 293	. 2 ⊢ (A ∈ D → (∀x∀y(y ∈ C → ∀x y ∈ C) ⋀ ∀x(x = A → B = C)))
6		csbiegft 2019	. . 3 ⊢ ((A ∈ D ⋀ ∀x∀y(y ∈ C → ∀x y ∈ C) ⋀ ∀x(x = A → B = C)) → [A / x]B = C)
7	6	3expb 832	. 2 ⊢ ((A ∈ D ⋀ (∀x∀y(y ∈ C → ∀x y ∈ C) ⋀ ∀x(x = A → B = C))) → [A / x]B = C)
8	5, 7	mpdan 702	1 ⊢ (A ∈ D → [A / x]B = C)

Syntax hints:   → wi 3   ⋀ wa 223  ∀wal 951   = wceq 953   ∈ wcel 955  [csb 1991

This theorem is referenced by:  csbima12g 3397  csbfv12g 3727  csboprg 3971  csbnegg 5336  fsum1p 6957

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-sbc 1932  df-csb 1992

Copyright terms: Public domain