Theorem bj-unirel

Description: Quantitative version of uniexr : if the union of a class is an element of a class, then that class is an element of the double powerclass of the union of this class. (Contributed by BJ, 6-Apr-2024)

	Ref	Expression
Assertion	bj-unirel	|- ( U. A e. V -> A e. ~P ~P U. V )

Proof

Step	Hyp	Ref	Expression
1		pwuni	|- A C_ ~P U. A
2		pwel	|- ( U. A e. V -> ~P U. A e. ~P ~P U. V )
3		bj-sselpwuni	|- ( ( A C_ ~P U. A /\ ~P U. A e. ~P ~P U. V ) -> A e. ~P U. ~P ~P U. V )
4	1 2 3	sylancr	|- ( U. A e. V -> A e. ~P U. ~P ~P U. V )
5		unipw	|- U. ~P ~P U. V = ~P U. V
6	5	pweqi	|- ~P U. ~P ~P U. V = ~P ~P U. V
7	4 6	eleqtrdi	|- ( U. A e. V -> A e. ~P ~P U. V )