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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	bj-elabd2ALT.eq	⊢ ( 𝜑 → 𝐵 = { 𝑥 ∣ 𝜓 } )
	bj-elabd2ALT.is	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	bj-elabd2ALT	⊢ ( 𝜑 → ( 𝐴 ∈ 𝐵 ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-elabd2ALT.ex	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		bj-elabd2ALT.eq	⊢ ( 𝜑 → 𝐵 = { 𝑥 ∣ 𝜓 } )
3		bj-elabd2ALT.is	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
4		simpr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → 𝑦 = 𝐴 )
5	2	eqcomd	⊢ ( 𝜑 → { 𝑥 ∣ 𝜓 } = 𝐵 )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → { 𝑥 ∣ 𝜓 } = 𝐵 )
7	4 6	eleq12d	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ 𝐴 ∈ 𝐵 ) )
8		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐴 ) )
9	8	biimparc	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝐴 )
10	9	anim2i	⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝐴 ∧ 𝑥 = 𝑦 ) ) → ( 𝜑 ∧ 𝑥 = 𝐴 ) )
11	10	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑦 = 𝐴 ) ∧ 𝑥 = 𝑦 ) → ( 𝜑 ∧ 𝑥 = 𝐴 ) )
12	11 3	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 = 𝐴 ) ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) )
13	12	sbiedvw	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ( [ 𝑦 / 𝑥 ] 𝜓 ↔ 𝜒 ) )
14	7 13	bibi12d	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ( ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( 𝐴 ∈ 𝐵 ↔ 𝜒 ) ) )
15		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑦 / 𝑥 ] 𝜓 )
16	15	a1i	⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑦 / 𝑥 ] 𝜓 ) )
17	1 14 16	vtocld	⊢ ( 𝜑 → ( 𝐴 ∈ 𝐵 ↔ 𝜒 ) )