Metamath Proof Explorer


Theorem wl-equsal1i

Description: The antecedent x = y is irrelevant, if one or both setvar variables are not free in ph . (Contributed by Wolf Lammen, 1-Sep-2018)

Ref Expression
Hypotheses wl-equsal1i.1
|- ( F/ x ph \/ F/ y ph )
wl-equsal1i.2
|- ( x = y -> ph )
Assertion wl-equsal1i
|- ph

Proof

Step Hyp Ref Expression
1 wl-equsal1i.1
 |-  ( F/ x ph \/ F/ y ph )
2 wl-equsal1i.2
 |-  ( x = y -> ph )
3 2 gen2
 |-  A. x A. y ( x = y -> ph )
4 sp
 |-  ( A. y A. x ( x = y -> ph ) -> A. x ( x = y -> ph ) )
5 4 alcoms
 |-  ( A. x A. y ( x = y -> ph ) -> A. x ( x = y -> ph ) )
6 wl-equsal1t
 |-  ( F/ x ph -> ( A. x ( x = y -> ph ) <-> ph ) )
7 5 6 syl5ib
 |-  ( F/ x ph -> ( A. x A. y ( x = y -> ph ) -> ph ) )
8 wl-equsalcom
 |-  ( A. y ( y = x -> ph ) <-> A. y ( x = y -> ph ) )
9 wl-equsal1t
 |-  ( F/ y ph -> ( A. y ( y = x -> ph ) <-> ph ) )
10 9 biimpd
 |-  ( F/ y ph -> ( A. y ( y = x -> ph ) -> ph ) )
11 8 10 syl5bir
 |-  ( F/ y ph -> ( A. y ( x = y -> ph ) -> ph ) )
12 11 spsd
 |-  ( F/ y ph -> ( A. x A. y ( x = y -> ph ) -> ph ) )
13 7 12 jaoi
 |-  ( ( F/ x ph \/ F/ y ph ) -> ( A. x A. y ( x = y -> ph ) -> ph ) )
14 1 3 13 mp2
 |-  ph