Metamath Proof Explorer

Theorem trsbcVD

Description: Formula-building inference rule for class substitution, substituting a class variable for the setvar 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 L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trsbc is trsbcVD without virtual deductions and was automatically derived from trsbcVD .

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.)

Ref Expression
Assertion trsbcVD ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] Tr 𝑥 ↔ Tr 𝐴 ) )

Proof

Step Hyp Ref Expression
1 idn1 ⊢ (    𝐴 ∈ 𝐵    ▶    𝐴 ∈ 𝐵    )
2 sbcg ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) )
3 1 2 e1a ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 )    )
4 sbcel2gv ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴 ) )
5 1 4 e1a ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴 )    )
6 sbcel2gv ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴 ) )
7 1 6 e1a ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴 )    )
8 imbi13 ⊢ ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) → ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴 ) → ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴 ) → ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 → [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ) ) ) )
9 8 a1i ⊢ ( 𝐴 ∈ 𝐵 → ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) → ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴 ) → ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴 ) → ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 → [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ) ) ) ) )
10 1 3 5 7 9 e1111 ⊢ (    𝐴 ∈ 𝐵    ▶    ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 → [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) )    )
11 sbcim2g ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 → [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ) ) ) )
12 1 11 e1a ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 → [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ) ) )    )
13 bibi1 ⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 → [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ) ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ) ↔ ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 → [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ) ) )
14 13 biimprcd ⊢ ( ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 → [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 → [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ) ) ) → ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ) ) )
15 10 12 14 e11 ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) )    )
16 pm3.31 ⊢ ( ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
17 pm3.3 ⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) → ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) )
18 16 17 impbii ⊢ ( ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
19 bibi1 ⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) ↔ ( ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) ) )
20 19 biimprd ⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ) → ( ( ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) → ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) ) )
21 15 18 20 e10 ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )    )
22 pm3.31 ⊢ ( ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
23 pm3.3 ⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) → ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) )
24 22 23 impbii ⊢ ( ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
25 24 ax-gen ⊢ ∀ 𝑥 ( ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
26 sbcbi ⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ( ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) → ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) ) )
27 1 25 26 e10 ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )    )
28 bitr3 ⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) → ( [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) ) )
29 28 com12 ⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) → ( [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) ) )
30 21 27 29 e11 ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )    )
31 30 gen11 ⊢ (    𝐴 ∈ 𝐵    ▶    ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )    )
32 albi ⊢ ( ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) → ( ∀ 𝑦 [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) )
33 31 32 e1a ⊢ (    𝐴 ∈ 𝐵    ▶    ( ∀ 𝑦 [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )    )
34 sbcal ⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
35 34 a1i ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) )
36 1 35 e1a ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )    )
37 bibi1 ⊢ ( ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) → ( ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) ↔ ( ∀ 𝑦 [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) ) )
38 37 biimprcd ⊢ ( ( ∀ 𝑦 [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) → ( ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) ) )
39 33 36 38 e11 ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )    )
40 39 gen11 ⊢ (    𝐴 ∈ 𝐵    ▶    ∀ 𝑧 ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )    )
41 albi ⊢ ( ∀ 𝑧 ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) → ( ∀ 𝑧 [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) )
42 40 41 e1a ⊢ (    𝐴 ∈ 𝐵    ▶    ( ∀ 𝑧 [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )    )
43 sbcal ⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
44 43 a1i ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) )
45 1 44 e1a ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )    )
46 bibi1 ⊢ ( ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) → ( ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) ↔ ( ∀ 𝑧 [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) ) )
47 46 biimprcd ⊢ ( ( ∀ 𝑧 [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) → ( ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) → ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) ) )
48 42 45 47 e11 ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )    )
49 dftr2 ⊢ ( Tr 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
50 biantr ⊢ ( ( ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( Tr 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) ) → ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ Tr 𝐴 ) )
51 50 ex ⊢ ( ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) → ( ( Tr 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) → ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ Tr 𝐴 ) ) )
52 48 49 51 e10 ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ Tr 𝐴 )    )
53 dftr2 ⊢ ( Tr 𝑥 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
54 53 ax-gen ⊢ ∀ 𝑥 ( Tr 𝑥 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
55 sbcbi ⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ( Tr 𝑥 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) → ( [ 𝐴 / 𝑥 ] Tr 𝑥 ↔ [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) ) )
56 1 54 55 e10 ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] Tr 𝑥 ↔ [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )    )
57 bibi1 ⊢ ( ( [ 𝐴 / 𝑥 ] Tr 𝑥 ↔ [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) → ( ( [ 𝐴 / 𝑥 ] Tr 𝑥 ↔ Tr 𝐴 ) ↔ ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ Tr 𝐴 ) ) )
58 57 biimprcd ⊢ ( ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ Tr 𝐴 ) → ( ( [ 𝐴 / 𝑥 ] Tr 𝑥 ↔ [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) → ( [ 𝐴 / 𝑥 ] Tr 𝑥 ↔ Tr 𝐴 ) ) )
59 52 56 58 e11 ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] Tr 𝑥 ↔ Tr 𝐴 )    )
60 59 in1 ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] Tr 𝑥 ↔ Tr 𝐴 ) )