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

Theorem trsbcVD 28330
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 27968 is trsbcVD 28330 without virtual deductions and was automatically derived from trsbcVD 28330.
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 28006 . . . . . . . . . . . . . 14  |-  (. A  e.  B  ->.  A  e.  B ).
2 biidd 229 . . . . . . . . . . . . . . . 16  |-  ( x  =  A  ->  (
z  e.  y  <->  z  e.  y ) )
32sbcieg 3136 . . . . . . . . . . . . . . 15  |-  ( A  e.  B  ->  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) )
41, 3e1_ 28069 . . . . . . . . . . . . . 14  |-  (. A  e.  B  ->.  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) ).
5 sbcel2gv 3164 . . . . . . . . . . . . . . 15  |-  ( A  e.  B  ->  ( [. A  /  x ]. y  e.  x  <->  y  e.  A ) )
61, 5e1_ 28069 . . . . . . . . . . . . . 14  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  x  <->  y  e.  A
) ).
7 sbcel2gv 3164 . . . . . . . . . . . . . . 15  |-  ( A  e.  B  ->  ( [. A  /  x ]. z  e.  x  <->  z  e.  A ) )
81, 7e1_ 28069 . . . . . . . . . . . . . 14  |-  (. A  e.  B  ->.  ( [. A  /  x ]. z  e.  x  <->  z  e.  A
) ).
9 imbi13 27947 . . . . . . . . . . . . . . 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 28117 . . . . . . . . . . . . 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 27966 . . . . . . . . . . . . . 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_ 28069 . . . . . . . . . . . . 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 28130 . . . . . . . . . . . 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 28136 . . . . . . . . . . 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 1552 . . . . . . . . . . . 12  |-  A. x
( ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( (
z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
27 sbcbi 27967 . . . . . . . . . . . 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 28136 . . . . . . . . . . 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 27936 . . . . . . . . . . . 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 28130 . . . . . . . . . 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 28058 . . . . . . . . 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 1570 . . . . . . . . 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_ 28069 . . . . . . . 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 3152 . . . . . . . . 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_ 28069 . . . . . . . 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 28130 . . . . . . 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 28058 . . . . . 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 1570 . . . . . 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_ 28069 . . . . 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 3152 . . . . . 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_ 28069 . . . . 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 28130 . . . 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 4245 . . . 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 28136 . . 3  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  Tr  A
) ).
52 dftr2 4245 . . . . 5  |-  ( Tr  x  <->  A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
5352ax-gen 1552 . . . 4  |-  A. x
( Tr  x  <->  A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
54 sbcbi 27967 . . . 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 28136 . . 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 28130 . 2  |-  (. A  e.  B  ->.  ( [. A  /  x ]. Tr  x  <->  Tr  A ) ).
5958in1 28003 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 1546    = wceq 1649    e. wcel 1717   [.wsbc 3104   Tr wtr 4243
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-sbc 3105  df-in 3270  df-ss 3277  df-uni 3958  df-tr 4244  df-vd1 28002
  Copyright terms: Public domain W3C validator