Theorem bj-19.41t

Description: Closed form of 19.41 from the same axioms as 19.41v . The same is doable with 19.27 , 19.28 , 19.31 , 19.32 , 19.44 , 19.45 . (Contributed by BJ, 2-Dec-2023)

	Ref	Expression
Assertion	bj-19.41t	|- ( F// x ps -> ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		exancom	|- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
2		bj-19.42t	|- ( F// x ps -> ( E. x ( ps /\ ph ) <-> ( ps /\ E. x ph ) ) )
3	1 2	syl5bb	|- ( F// x ps -> ( E. x ( ph /\ ps ) <-> ( ps /\ E. x ph ) ) )
4	3	biancomd	|- ( F// x ps -> ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) ) )