Metamath Proof Explorer


Theorem sbciegft

Description: Conversion of implicit substitution to explicit class substitution, using a bound-variable hypothesis instead of distinct variables. (Closed theorem version of sbciegf .) (Contributed by NM, 10-Nov-2005) (Revised by Mario Carneiro, 13-Oct-2016)

Ref Expression
Assertion sbciegft AVxψxx=Aφψ[˙A/x]˙φψ

Proof

Step Hyp Ref Expression
1 sbc5 [˙A/x]˙φxx=Aφ
2 biimp φψφψ
3 2 imim2i x=Aφψx=Aφψ
4 3 impd x=Aφψx=Aφψ
5 4 alimi xx=Aφψxx=Aφψ
6 19.23t xψxx=Aφψxx=Aφψ
7 6 biimpa xψxx=Aφψxx=Aφψ
8 5 7 sylan2 xψxx=Aφψxx=Aφψ
9 8 3adant1 AVxψxx=Aφψxx=Aφψ
10 1 9 syl5bi AVxψxx=Aφψ[˙A/x]˙φψ
11 biimpr φψψφ
12 11 imim2i x=Aφψx=Aψφ
13 12 com23 x=Aφψψx=Aφ
14 13 alimi xx=Aφψxψx=Aφ
15 19.21t xψxψx=Aφψxx=Aφ
16 15 biimpa xψxψx=Aφψxx=Aφ
17 14 16 sylan2 xψxx=Aφψψxx=Aφ
18 17 3adant1 AVxψxx=Aφψψxx=Aφ
19 sbc6g AV[˙A/x]˙φxx=Aφ
20 19 3ad2ant1 AVxψxx=Aφψ[˙A/x]˙φxx=Aφ
21 18 20 sylibrd AVxψxx=Aφψψ[˙A/x]˙φ
22 10 21 impbid AVxψxx=Aφψ[˙A/x]˙φψ