Theorem bj-sbsb

Description: Biconditional showing two possible (dual) definitions of substitution df-sb not using dummy variables. (Contributed by BJ, 19-Mar-2021)

	Ref	Expression
Assertion	bj-sbsb	|- ( ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) <-> ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) -> ( x = y -> ph ) )
2		pm2.27	|- ( x = y -> ( ( x = y -> ph ) -> ph ) )
3	2	anc2li	|- ( x = y -> ( ( x = y -> ph ) -> ( x = y /\ ph ) ) )
4	3	sps	|- ( A. x x = y -> ( ( x = y -> ph ) -> ( x = y /\ ph ) ) )
5		olc	|- ( ( x = y /\ ph ) -> ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) )
6	1 4 5	syl56	|- ( A. x x = y -> ( ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) -> ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) ) )
7		simpr	|- ( ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) -> E. x ( x = y /\ ph ) )
8		equs5	|- ( -. A. x x = y -> ( E. x ( x = y /\ ph ) <-> A. x ( x = y -> ph ) ) )
9	8	biimpd	|- ( -. A. x x = y -> ( E. x ( x = y /\ ph ) -> A. x ( x = y -> ph ) ) )
10		orc	|- ( A. x ( x = y -> ph ) -> ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) )
11	7 9 10	syl56	|- ( -. A. x x = y -> ( ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) -> ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) ) )
12	6 11	pm2.61i	|- ( ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) -> ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) )
13		sp	|- ( A. x ( x = y -> ph ) -> ( x = y -> ph ) )
14		pm3.4	|- ( ( x = y /\ ph ) -> ( x = y -> ph ) )
15	13 14	jaoi	|- ( ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) -> ( x = y -> ph ) )
16		equs4	|- ( A. x ( x = y -> ph ) -> E. x ( x = y /\ ph ) )
17		19.8a	|- ( ( x = y /\ ph ) -> E. x ( x = y /\ ph ) )
18	16 17	jaoi	|- ( ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) -> E. x ( x = y /\ ph ) )
19	15 18	jca	|- ( ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) -> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
20	12 19	impbii	|- ( ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) <-> ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) )