Theorem bj-elabd2ALT

Description: Alternate proof of elabd2 bypassing elab6g (and using sbiedvw instead of the A. x ( x = y -> ps ) idiom). (Contributed by BJ, 16-Oct-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bj-elabd2ALT.ex	|- ( ph -> A e. V )
	bj-elabd2ALT.eq	|- ( ph -> B = { x | ps } )
	bj-elabd2ALT.is	|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
Assertion	bj-elabd2ALT	|- ( ph -> ( A e. B <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		bj-elabd2ALT.ex	|- ( ph -> A e. V )
2		bj-elabd2ALT.eq	|- ( ph -> B = { x | ps } )
3		bj-elabd2ALT.is	|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
4		simpr	|- ( ( ph /\ y = A ) -> y = A )
5	2	eqcomd	|- ( ph -> { x | ps } = B )
6	5	adantr	|- ( ( ph /\ y = A ) -> { x | ps } = B )
7	4 6	eleq12d	|- ( ( ph /\ y = A ) -> ( y e. { x | ps } <-> A e. B ) )
8		eqeq1	|- ( x = y -> ( x = A <-> y = A ) )
9	8	biimparc	|- ( ( y = A /\ x = y ) -> x = A )
10	9	anim2i	|- ( ( ph /\ ( y = A /\ x = y ) ) -> ( ph /\ x = A ) )
11	10	anassrs	|- ( ( ( ph /\ y = A ) /\ x = y ) -> ( ph /\ x = A ) )
12	11 3	syl	|- ( ( ( ph /\ y = A ) /\ x = y ) -> ( ps <-> ch ) )
13	12	sbiedvw	|- ( ( ph /\ y = A ) -> ( [ y / x ] ps <-> ch ) )
14	7 13	bibi12d	|- ( ( ph /\ y = A ) -> ( ( y e. { x | ps } <-> [ y / x ] ps ) <-> ( A e. B <-> ch ) ) )
15		df-clab	|- ( y e. { x | ps } <-> [ y / x ] ps )
16	15	a1i	|- ( ph -> ( y e. { x | ps } <-> [ y / x ] ps ) )
17	1 14 16	vtocld	|- ( ph -> ( A e. B <-> ch ) )