Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  trsbcVD Structured version   Unicode version

Theorem trsbcVD 28926
Description: Formula-building inference rule for class substitution, substituting a class variable for the set variable of the transitivity predicate. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trsbc 28562 is trsbcVD 28926 without virtual deductions and was automatically derived from trsbcVD 28926.
1::  |-  (. A  e.  B  ->.  A  e.  B ).
2:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) ).
3:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  x  <->  y  e.  A ) ).
4:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. z  e.  x  <->  z  e.  A ) ).
5:1,2,3,4:  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) ).
6:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) ) ) ).
7:5,6:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) ).
8::  |-  ( ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
9:7,8:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
10::  |-  ( ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
11:10:  |-  A. x ( ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
12:1,11:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
13:9,12:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
14:13:  |-  (. A  e.  B  ->.  A. y ( [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
15:14:  |-  (. A  e.  B  ->.  ( A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
16:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
17:15,16:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
18:17:  |-  (. A  e.  B  ->.  A. z ( [. A  /  x ]. A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
19:18:  |-  (. A  e.  B  ->.  ( A. z [. A  /  x ]. A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
20:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. z A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
21:19,20:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. z A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
22::  |-  ( Tr  A  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
23:21,22:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. z A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  Tr  A ) ).
24::  |-  ( Tr  x  <->  A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
25:24:  |-  A. x ( Tr  x  <->  A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
26:1,25:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. Tr  x  <->  [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
27:23,26:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. Tr  x  <->  Tr  A ) ).
qed:27:  |-  ( A  e.  B  ->  ( [. A  /  x ]. Tr  x  <->  Tr  A ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
trsbcVD  |-  ( A  e.  B  ->  ( [. A  /  x ]. Tr  x  <->  Tr  A
) )
Distinct variable group:    x, A
Allowed substitution hint:    B( x)

Proof of Theorem trsbcVD
Dummy variables  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn1 28602 . . . . . . . . . . . . . 14  |-  (. A  e.  B  ->.  A  e.  B ).
2 biidd 229 . . . . . . . . . . . . . . . 16  |-  ( x  =  A  ->  (
z  e.  y  <->  z  e.  y ) )
32sbcieg 3185 . . . . . . . . . . . . . . 15  |-  ( A  e.  B  ->  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) )
41, 3e1_ 28665 . . . . . . . . . . . . . 14  |-  (. A  e.  B  ->.  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) ).
5 sbcel2gv 3213 . . . . . . . . . . . . . . 15  |-  ( A  e.  B  ->  ( [. A  /  x ]. y  e.  x  <->  y  e.  A ) )
61, 5e1_ 28665 . . . . . . . . . . . . . 14  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  x  <->  y  e.  A
) ).
7 sbcel2gv 3213 . . . . . . . . . . . . . . 15  |-  ( A  e.  B  ->  ( [. A  /  x ]. z  e.  x  <->  z  e.  A ) )
81, 7e1_ 28665 . . . . . . . . . . . . . 14  |-  (. A  e.  B  ->.  ( [. A  /  x ]. z  e.  x  <->  z  e.  A
) ).
9 imbi13 28541 . . . . . . . . . . . . . . 15  |-  ( (
[. A  /  x ]. z  e.  y  <->  z  e.  y )  -> 
( ( [. A  /  x ]. y  e.  x  <->  y  e.  A
)  ->  ( ( [. A  /  x ]. z  e.  x  <->  z  e.  A )  -> 
( ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) ) ) )
109a1i 11 . . . . . . . . . . . . . 14  |-  ( A  e.  B  ->  (
( [. A  /  x ]. z  e.  y  <->  z  e.  y )  -> 
( ( [. A  /  x ]. y  e.  x  <->  y  e.  A
)  ->  ( ( [. A  /  x ]. z  e.  x  <->  z  e.  A )  -> 
( ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) ) ) ) )
111, 4, 6, 8, 10e1111 28713 . . . . . . . . . . . . 13  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) ).
12 sbcim2g 28560 . . . . . . . . . . . . . 14  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) ) ) )
131, 12e1_ 28665 . . . . . . . . . . . . 13  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  (
y  e.  x  -> 
z  e.  x ) )  <->  ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) ) ) ).
14 bibi1 318 . . . . . . . . . . . . . 14  |-  ( (
[. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) ) )  ->  ( ( [. A  /  x ]. (
z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) )  <-> 
( ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) ) )
1514biimprcd 217 . . . . . . . . . . . . 13  |-  ( ( ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x
) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) )  ->  ( ( [. A  /  x ]. (
z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) )  <->  ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) ) )  ->  ( [. A  /  x ]. ( z  e.  y  ->  (
y  e.  x  -> 
z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) ) )
1611, 13, 15e11 28726 . . . . . . . . . . . 12  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  (
y  e.  x  -> 
z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) ).
17 pm3.31 433 . . . . . . . . . . . . 13  |-  ( ( z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) )  ->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
18 pm3.3 432 . . . . . . . . . . . . 13  |-  ( ( ( z  e.  y  /\  y  e.  A
)  ->  z  e.  A )  ->  (
z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) ) )
1917, 18impbii 181 . . . . . . . . . . . 12  |-  ( ( z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
20 bibi1 318 . . . . . . . . . . . . 13  |-  ( (
[. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) )  ->  ( ( [. A  /  x ]. (
z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )  <->  ( (
z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ) )
2120biimprd 215 . . . . . . . . . . . 12  |-  ( (
[. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) )  ->  ( ( ( z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )  -> 
( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ) )
2216, 19, 21e10 28732 . . . . . . . . . . 11  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  (
y  e.  x  -> 
z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
23 pm3.31 433 . . . . . . . . . . . . . 14  |-  ( ( z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) )  ->  ( (
z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
24 pm3.3 432 . . . . . . . . . . . . . 14  |-  ( ( ( z  e.  y  /\  y  e.  x
)  ->  z  e.  x )  ->  (
z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) ) )
2523, 24impbii 181 . . . . . . . . . . . . 13  |-  ( ( z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
2625ax-gen 1555 . . . . . . . . . . . 12  |-  A. x
( ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( (
z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
27 sbcbi 28561 . . . . . . . . . . . 12  |-  ( A  e.  B  ->  ( A. x ( ( z  e.  y  ->  (
y  e.  x  -> 
z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )  -> 
( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ) )
281, 26, 27e10 28732 . . . . . . . . . . 11  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  (
y  e.  x  -> 
z  e.  x ) )  <->  [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
29 bitr3 28530 . . . . . . . . . . . 12  |-  ( (
[. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )  -> 
( ( [. A  /  x ]. ( z  e.  y  ->  (
y  e.  x  -> 
z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )  -> 
( [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ) )
3029com12 29 . . . . . . . . . . 11  |-  ( (
[. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )  ->  ( ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )  -> 
( [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ) )
3122, 28, 30e11 28726 . . . . . . . . . 10  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <-> 
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
3231gen11 28654 . . . . . . . . 9  |-  (. A  e.  B  ->.  A. y ( [. A  /  x ]. (
( z  e.  y  /\  y  e.  x
)  ->  z  e.  x )  <->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
33 albi 1573 . . . . . . . . 9  |-  ( A. y ( [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <-> 
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )  -> 
( A. y [. A  /  x ]. (
( z  e.  y  /\  y  e.  x
)  ->  z  e.  x )  <->  A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) )
3432, 33e1_ 28665 . . . . . . . 8  |-  (. A  e.  B  ->.  ( A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
35 sbcalg 3201 . . . . . . . . 9  |-  ( A  e.  B  ->  ( [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) )
361, 35e1_ 28665 . . . . . . . 8  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
37 bibi1 318 . . . . . . . . 9  |-  ( (
[. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )  -> 
( ( [. A  /  x ]. A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )  <->  ( A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ) )
3837biimprcd 217 . . . . . . . 8  |-  ( ( A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )  -> 
( ( [. A  /  x ]. A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )  -> 
( [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ) )
3934, 36, 38e11 28726 . . . . . . 7  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
4039gen11 28654 . . . . . 6  |-  (. A  e.  B  ->.  A. z ( [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
41 albi 1573 . . . . . 6  |-  ( A. z ( [. A  /  x ]. A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )  -> 
( A. z [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) )
4240, 41e1_ 28665 . . . . 5  |-  (. A  e.  B  ->.  ( A. z [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A
)  ->  z  e.  A ) ) ).
43 sbcalg 3201 . . . . . 6  |-  ( A  e.  B  ->  ( [. A  /  x ]. A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) )
441, 43e1_ 28665 . . . . 5  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
45 bibi1 318 . . . . . 6  |-  ( (
[. A  /  x ]. A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )  ->  ( ( [. A  /  x ]. A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )  <->  ( A. z [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A
)  ->  z  e.  A ) ) ) )
4645biimprcd 217 . . . . 5  |-  ( ( A. z [. A  /  x ]. A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )  -> 
( ( [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )  ->  ( [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A
)  ->  z  e.  A ) ) ) )
4742, 44, 46e11 28726 . . . 4  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
48 dftr2 4296 . . . 4  |-  ( Tr  A  <->  A. z A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
49 biantr 898 . . . . 5  |-  ( ( ( [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )  /\  ( Tr  A  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) )  ->  ( [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  Tr  A
) )
5049ex 424 . . . 4  |-  ( (
[. A  /  x ]. A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )  -> 
( ( Tr  A  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A
)  ->  z  e.  A ) )  -> 
( [. A  /  x ]. A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  Tr  A
) ) )
5147, 48, 50e10 28732 . . 3  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  Tr  A
) ).
52 dftr2 4296 . . . . 5  |-  ( Tr  x  <->  A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
5352ax-gen 1555 . . . 4  |-  A. x
( Tr  x  <->  A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
54 sbcbi 28561 . . . 4  |-  ( A  e.  B  ->  ( A. x ( Tr  x  <->  A. z A. y ( ( z  e.  y  /\  y  e.  x
)  ->  z  e.  x ) )  -> 
( [. A  /  x ]. Tr  x  <->  [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ) )
551, 53, 54e10 28732 . . 3  |-  (. A  e.  B  ->.  ( [. A  /  x ]. Tr  x  <->  [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x
)  ->  z  e.  x ) ) ).
56 bibi1 318 . . . 4  |-  ( (
[. A  /  x ]. Tr  x  <->  [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )  -> 
( ( [. A  /  x ]. Tr  x  <->  Tr  A )  <->  ( [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  Tr  A ) ) )
5756biimprcd 217 . . 3  |-  ( (
[. A  /  x ]. A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  Tr  A
)  ->  ( ( [. A  /  x ]. Tr  x  <->  [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )  -> 
( [. A  /  x ]. Tr  x  <->  Tr  A
) ) )
5851, 55, 57e11 28726 . 2  |-  (. A  e.  B  ->.  ( [. A  /  x ]. Tr  x  <->  Tr  A ) ).
5958in1 28599 1  |-  ( A  e.  B  ->  ( [. A  /  x ]. Tr  x  <->  Tr  A
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549    = wceq 1652    e. wcel 1725   [.wsbc 3153   Tr wtr 4294
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-sbc 3154  df-in 3319  df-ss 3326  df-uni 4008  df-tr 4295  df-vd1 28598
  Copyright terms: Public domain W3C validator