Metamath Proof Explorer


Theorem disjenex

Description: Existence version of disjen . (Contributed by Mario Carneiro, 7-Feb-2015)

Ref Expression
Assertion disjenex AVBWxAx=xB

Proof

Step Hyp Ref Expression
1 simpr AVBWBW
2 snex 𝒫ranAV
3 xpexg BW𝒫ranAVB×𝒫ranAV
4 1 2 3 sylancl AVBWB×𝒫ranAV
5 disjen AVBWAB×𝒫ranA=B×𝒫ranAB
6 ineq2 x=B×𝒫ranAAx=AB×𝒫ranA
7 6 eqeq1d x=B×𝒫ranAAx=AB×𝒫ranA=
8 breq1 x=B×𝒫ranAxBB×𝒫ranAB
9 7 8 anbi12d x=B×𝒫ranAAx=xBAB×𝒫ranA=B×𝒫ranAB
10 4 5 9 spcedv AVBWxAx=xB