Metamath Proof Explorer

Theorem csbrngVD

Description: Virtual deduction proof of csbrn . 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. csbrn is csbrngVD without virtual deductions and was automatically derived from csbrngVD .

1:: |- (. A e. V ->. A e. V ).
2:1: |- (. A e. V ->. ( [. A / x ]. <. w ,. y >. e. B <-> [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B ) ).
3:1: |- (. A e. V ->. [_ A / x ]_ <. w ,. y >. = <. w , y >. ).
4:3: |- (. A e. V ->. ( [_ A / x ]_ <. w ,. y >. e. [_ A / x ]_ B <-> <. w , y >. e. [_ A / x ]_ B ) ).
5:2,4: |- (. A e. V ->. ( [. A / x ]. <. w ,. y >. e. B <-> <. w , y >. e. [_ A / x ]_ B ) ).
6:5: |- (. A e. V ->. A. w ( [. A / x ]. <. w ,. y >. e. B <-> <. w , y >. e. [_ A / x ]_ B ) ).
7:6: |- (. A e. V ->. ( E. w [. A / x ]. <. w ,. y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ).
8:1: |- (. A e. V ->. ( E. w [. A / x ]. <. w ,. y >. e. B <-> [. A / x ]. E. w <. w , y >. e. B ) ).
9:7,8: |- (. A e. V ->. ( [. A / x ]. E. w <. w ,. y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ).
10:9: |- (. A e. V ->. A. y ( [. A / x ]. E. w <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ).
11:10: |- (. A e. V ->. { y | [. A / x ]. E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } ).
12:1: |- (. A e. V ->. [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | [. A / x ]. E. w <. w , y >. e. B } ).
13:11,12: |- (. A e. V ->. [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } ).
14:: |- ran B = { y | E. w <. w ,. y >. e. B }
15:14: |- A. x ran B = { y | E. w <. w ,. y >. e. B }
16:1,15: |- (. A e. V ->. [_ A / x ]_ ran B = [_ A / x ]_ { y | E. w <. w , y >. e. B } ).
17:13,16: |- (. A e. V ->. [_ A / x ]_ ran B = { y | E. w <. w , y >. e. [_ A / x ]_ B } ).
18:: |- ran [_ A / x ]_ B = { y | E. w <. w ,. y >. e. [_ A / x ]_ B }
19:17,18: |- (. A e. V ->. [_ A / x ]_ ran B = ran [_ A / x ]_ B ).
qed:19: |- ( A e. V -> [_ A / x ]_ ran B = ran [_ A / x ]_ B )
(Contributed by Alan Sare, 10-Nov-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion csbrngVD ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )

Proof

Step Hyp Ref Expression
1 idn1 ⊢ (    𝐴 ∈ 𝑉    ▶    𝐴 ∈ 𝑉    )
2 sbcel12 ⊢ ( [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
3 2 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
4 1 3 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ( [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )    )
5 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑤 , 𝑦 ⟩ = ⟨ 𝑤 , 𝑦 ⟩ )
6 1 5 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑤 , 𝑦 ⟩ = ⟨ 𝑤 , 𝑦 ⟩    )
7 eleq1 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑤 , 𝑦 ⟩ = ⟨ 𝑤 , 𝑦 ⟩ → ( ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
8 6 7 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ( ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )    )
9 bibi1 ⊢ ( ( [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( ( [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ↔ ( ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) )
10 9 biimprd ⊢ ( ( [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( ( ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) )
11 4 8 10 e11 ⊢ (    𝐴 ∈ 𝑉    ▶    ( [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )    )
12 11 gen11 ⊢ (    𝐴 ∈ 𝑉    ▶    ∀ 𝑤 ( [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )    )
13 exbi ⊢ ( ∀ 𝑤 ( [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
14 12 13 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )    )
15 sbcex2 ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 )
16 15 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ) )
17 16 bicomd ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ) )
18 1 17 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 )    )
19 bitr3 ⊢ ( ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ) → ( ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) )
20 19 com12 ⊢ ( ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ) → ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) )
21 14 18 20 e11 ⊢ (    𝐴 ∈ 𝑉    ▶    ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )    )
22 21 gen11 ⊢ (    𝐴 ∈ 𝑉    ▶    ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )    )
23 abbi ⊢ ( ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ↔ { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } )
24 23 biimpi ⊢ ( ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } )
25 22 24 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 }    )
26 csbab ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 }
27 26 a1i ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } )
28 1 27 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 }    )
29 eqeq2 ⊢ ( { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } ↔ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) )
30 29 biimpd ⊢ ( { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } → ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) )
31 25 28 30 e11 ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 }    )
32 dfrn3 ⊢ ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 }
33 32 ax-gen ⊢ ∀ 𝑥 ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 }
34 csbeq2 ⊢ ( ∀ 𝑥 ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } → ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } )
35 34 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } → ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } ) )
36 1 33 35 e10 ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 }    )
37 eqeq2 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ( ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } ↔ ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) )
38 37 biimpd ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ( ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ 𝐵 } → ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) )
39 31 36 38 e11 ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 }    )
40 dfrn3 ⊢ ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 }
41 eqeq2 ⊢ ( ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ( ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) )
42 41 biimprcd ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ( ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑤 , 𝑦 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
43 39 40 42 e10 ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵    )
44 43 in1 ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )