Theorem csbrngVD 45002

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

1::	⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]⟨𝑤   ,   𝑦⟩ ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
3:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌⟨𝑤   ,   𝑦⟩ = ⟨𝑤, 𝑦⟩   )
4:3:	⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌⟨𝑤   ,   𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
5:2,4:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]⟨𝑤   ,   𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
6:5:	⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑤([𝐴 / 𝑥]⟨𝑤   ,    𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
7:6:	⊢ (   𝐴 ∈ 𝑉   ▶   (∃𝑤[𝐴 / 𝑥]⟨𝑤   ,    𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
8:1:	⊢ (   𝐴 ∈ 𝑉   ▶   (∃𝑤[𝐴 / 𝑥]⟨𝑤   ,    𝑦⟩ ∈ 𝐵 ↔ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵)   )
9:7,8:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]∃𝑤⟨𝑤    ,   𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
10:9:	⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑦([𝐴 / 𝑥]∃𝑤 ⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
11:10:	⊢ (   𝐴 ∈ 𝑉   ▶   {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨ 𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}   )
12:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤 ⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}   )
13:11,12:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤 ⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}   )
14::	⊢ ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤   ,   𝑦⟩ ∈ 𝐵}
15:14:	⊢ ∀𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤   ,   𝑦⟩ ∈ 𝐵}
16:1,15:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}   )
17:13,16:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}   )
18::	⊢ ran ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤    ,   𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}
19:17,18:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋ 𝐴 / 𝑥⦌𝐵   )
qed:19:	⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵)

(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

Proof of Theorem csbrngVD

Dummy variables 𝑤 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		idn1 44681	. . . . . . . . . . . 12 ⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2		sbcel12 4362	. . . . . . . . . . . . 13 ⊢ ([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)
3	2	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵))
4	1, 3	e1a 44734	. . . . . . . . . . 11 ⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
5		csbconstg 3866	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ = ⟨𝑤, 𝑦⟩)
6	1, 5	e1a 44734	. . . . . . . . . . . 12 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ = ⟨𝑤, 𝑦⟩   )
7		eleq1 2821	. . . . . . . . . . . 12 ⊢ (⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ = ⟨𝑤, 𝑦⟩ → (⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵))
8	6, 7	e1a 44734	. . . . . . . . . . 11 ⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
9		bibi1 351	. . . . . . . . . . . 12 ⊢ (([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) → (([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) ↔ (⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)))
10	9	biimprd 248	. . . . . . . . . . 11 ⊢ (([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) → ((⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) → ([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)))
11	4, 8, 10	e11 44795	. . . . . . . . . 10 ⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
12	11	gen11 44723	. . . . . . . . 9 ⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑤([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
13		exbi 1848	. . . . . . . . 9 ⊢ (∀𝑤([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) → (∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵))
14	12, 13	e1a 44734	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝑉   ▶   (∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
15		sbcex2 3799	. . . . . . . . . . 11 ⊢ ([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵)
16	15	a1i 11	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵))
17	16	bicomd 223	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → (∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵))
18	1, 17	e1a 44734	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝑉   ▶   (∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵)   )
19		bitr3 352	. . . . . . . . 9 ⊢ ((∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵) → ((∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) → ([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)))
20	19	com12 32	. . . . . . . 8 ⊢ ((∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) → ((∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵) → ([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)))
21	14, 18, 20	e11 44795	. . . . . . 7 ⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
22	21	gen11 44723	. . . . . 6 ⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑦([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
23		abbib 2802	. . . . . . 7 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} ↔ ∀𝑦([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵))
24	23	biimpri 228	. . . . . 6 ⊢ (∀𝑦([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) → {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵})
25	22, 24	e1a 44734	. . . . 5 ⊢ (   𝐴 ∈ 𝑉   ▶   {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}   )
26		csbab 4391	. . . . . . 7 ⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}
27	26	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵})
28	1, 27	e1a 44734	. . . . 5 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}   )
29		eqeq2 2745	. . . . . 6 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} ↔ ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}))
30	29	biimpd 229	. . . . 5 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} → ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}))
31	25, 28, 30	e11 44795	. . . 4 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}   )
32		dfrn3 5836	. . . . . 6 ⊢ ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}
33	32	ax-gen 1796	. . . . 5 ⊢ ∀𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}
34		csbeq2 3852	. . . . . 6 ⊢ (∀𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} → ⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵})
35	34	a1i 11	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} → ⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}))
36	1, 33, 35	e10 44801	. . . 4 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}   )
37		eqeq2 2745	. . . . 5 ⊢ (⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} ↔ ⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}))
38	37	biimpd 229	. . . 4 ⊢ (⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} → ⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}))
39	31, 36, 38	e11 44795	. . 3 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}   )
40		dfrn3 5836	. . 3 ⊢ ran ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}
41		eqeq2 2745	. . . 4 ⊢ (ran ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵 ↔ ⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}))
42	41	biimprcd 250	. . 3 ⊢ (⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} → (ran ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵))
43	39, 40, 42	e10 44801	. 2 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵   )
44	43	in1 44678	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2113  {cab 2711  [wsbc 3738  ⦋csb 3847  ⟨cop 4583  ran crn 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-cnv 5629  df-dm 5631  df-rn 5632  df-vd1 44677

This theorem is referenced by: (None)