This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rspc2vd

Description: Deduction version of 2-variable restricted specialization, using implicit substitution. Notice that the class D for the second set variable y may depend on the first set variable x . (Contributed by AV, 29-Mar-2021)

Ref Expression
Hypotheses rspc2vd.a 
|- ( x = A -> ( th <-> ch ) )
rspc2vd.b 
|- ( y = B -> ( ch <-> ps ) )
rspc2vd.c 
|- ( ph -> A e. C )
rspc2vd.d 
|- ( ( ph /\ x = A ) -> D = E )
rspc2vd.e 
|- ( ph -> B e. E )
Assertion rspc2vd 
|- ( ph -> ( A. x e. C A. y e. D th -> ps ) )

Proof

Step Hyp Ref Expression
1 rspc2vd.a 
 |-  ( x = A -> ( th <-> ch ) )
2 rspc2vd.b 
 |-  ( y = B -> ( ch <-> ps ) )
3 rspc2vd.c 
 |-  ( ph -> A e. C )
4 rspc2vd.d 
 |-  ( ( ph /\ x = A ) -> D = E )
5 rspc2vd.e 
 |-  ( ph -> B e. E )
6 3 4 csbied 
 |-  ( ph -> [_ A / x ]_ D = E )
7 5 6 eleqtrrd 
 |-  ( ph -> B e. [_ A / x ]_ D )
8 nfcsb1v 
 |-  F/_ x [_ A / x ]_ D
9 nfv 
 |-  F/ x ch
10 8 9 nfralw 
 |-  F/ x A. y e. [_ A / x ]_ D ch
11 csbeq1a 
 |-  ( x = A -> D = [_ A / x ]_ D )
12 11 1 raleqbidv 
 |-  ( x = A -> ( A. y e. D th <-> A. y e. [_ A / x ]_ D ch ) )
13 10 12 rspc 
 |-  ( A e. C -> ( A. x e. C A. y e. D th -> A. y e. [_ A / x ]_ D ch ) )
14 3 13 syl 
 |-  ( ph -> ( A. x e. C A. y e. D th -> A. y e. [_ A / x ]_ D ch ) )
15 2 rspcv 
 |-  ( B e. [_ A / x ]_ D -> ( A. y e. [_ A / x ]_ D ch -> ps ) )
16 7 14 15 sylsyld 
 |-  ( ph -> ( A. x e. C A. y e. D th -> ps ) )