Theorem cnvtrucl0

Description: The converse of the trivial closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020)

	Ref	Expression
Assertion	cnvtrucl0	|- ( X e. V -> `' |^| { x | ( X C_ x /\ T. ) } = |^| { y | ( `' X C_ y /\ T. ) } )

Proof

Step	Hyp	Ref	Expression
1		idd	|- ( ( X e. V /\ x = ( `' y u. ( X \ `' `' X ) ) ) -> ( T. -> T. ) )
2		idd	|- ( ( X e. V /\ y = `' x ) -> ( T. -> T. ) )
3		biidd	|- ( x = X -> ( T. <-> T. ) )
4		ssidd	|- ( X e. V -> X C_ X )
5		elex	|- ( X e. V -> X e. _V )
6		trud	|- ( X e. V -> T. )
7	1 2 3 4 5 6	clcnvlem	|- ( X e. V -> `' |^| { x | ( X C_ x /\ T. ) } = |^| { y | ( `' X C_ y /\ T. ) } )