Metamath Proof Explorer

Theorem disjlem19

Description: Lemma for disjdmqseq , partim2 and petlem via disjdmqs , (general version of the former prtlem19 ). (Contributed by Peter Mazsa, 16-Sep-2021)

Ref Expression
Assertion disjlem19 
|- ( A e. V -> ( Disj R -> ( ( x e. dom R /\ A e. [ x ] R ) -> [ x ] R = [ A ] ,~ R ) ) )

Proof

Step Hyp Ref Expression
1 disjlem18 
 |-  ( ( A e. V /\ z e. _V ) -> ( Disj R -> ( ( x e. dom R /\ A e. [ x ] R ) -> ( z e. [ x ] R <-> A ,~ R z ) ) ) )
2 1 elvd 
 |-  ( A e. V -> ( Disj R -> ( ( x e. dom R /\ A e. [ x ] R ) -> ( z e. [ x ] R <-> A ,~ R z ) ) ) )
3 2 imp31 
 |-  ( ( ( A e. V /\ Disj R ) /\ ( x e. dom R /\ A e. [ x ] R ) ) -> ( z e. [ x ] R <-> A ,~ R z ) )
4 elecALTV 
 |-  ( ( A e. V /\ z e. _V ) -> ( z e. [ A ] ,~ R <-> A ,~ R z ) )
5 4 elvd 
 |-  ( A e. V -> ( z e. [ A ] ,~ R <-> A ,~ R z ) )
6 5 ad2antrr 
 |-  ( ( ( A e. V /\ Disj R ) /\ ( x e. dom R /\ A e. [ x ] R ) ) -> ( z e. [ A ] ,~ R <-> A ,~ R z ) )
7 3 6 bitr4d 
 |-  ( ( ( A e. V /\ Disj R ) /\ ( x e. dom R /\ A e. [ x ] R ) ) -> ( z e. [ x ] R <-> z e. [ A ] ,~ R ) )
8 7 eqrdv 
 |-  ( ( ( A e. V /\ Disj R ) /\ ( x e. dom R /\ A e. [ x ] R ) ) -> [ x ] R = [ A ] ,~ R )
9 8 exp31 
 |-  ( A e. V -> ( Disj R -> ( ( x e. dom R /\ A e. [ x ] R ) -> [ x ] R = [ A ] ,~ R ) ) )