Theorem disjsuc2

Description: Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023)

	Ref	Expression
Assertion	disjsuc2	|- ( A e. V -> ( A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) /\ A. u e. A ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		disjressuc2	|- ( A e. V -> ( A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) /\ A. u e. A ( [ u ] ( R |X. `' _E ) i^i [ A ] ( R |X. `' _E ) ) = (/) ) ) )
2		disjecxrncnvep	|- ( ( u e. _V /\ A e. V ) -> ( ( [ u ] ( R |X. `' _E ) i^i [ A ] ( R |X. `' _E ) ) = (/) <-> ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) )
3	2	el2v1	|- ( A e. V -> ( ( [ u ] ( R |X. `' _E ) i^i [ A ] ( R |X. `' _E ) ) = (/) <-> ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) )
4	3	ralbidv	|- ( A e. V -> ( A. u e. A ( [ u ] ( R |X. `' _E ) i^i [ A ] ( R |X. `' _E ) ) = (/) <-> A. u e. A ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) )
5	4	anbi2d	|- ( A e. V -> ( ( A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) /\ A. u e. A ( [ u ] ( R |X. `' _E ) i^i [ A ] ( R |X. `' _E ) ) = (/) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) /\ A. u e. A ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) ) )
6	1 5	bitrd	|- ( A e. V -> ( A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) /\ A. u e. A ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) ) )