Theorem csbrngVD 45574

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

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 45253	. . . . . . . . . . . 12 ⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2		sbcel12 4375	. . . . . . . . . . . . 13 ⊢ ([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)
3	2	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵))
4	1, 3	e1a 45306	. . . . . . . . . . 11 ⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
5		csbconstg 3871	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ = ⟨𝑤, 𝑦⟩)
6	1, 5	e1a 45306	. . . . . . . . . . . 12 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ = ⟨𝑤, 𝑦⟩   )
7		eleq1 2849	. . . . . . . . . . . 12 ⊢ (⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ = ⟨𝑤, 𝑦⟩ → (⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵))
8	6, 7	e1a 45306	. . . . . . . . . . 11 ⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
9		bibi1 354	. . . . . . . . . . . 12 ⊢ (([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) → (([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) ↔ (⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)))
10	9	biimprd 251	. . . . . . . . . . 11 ⊢ (([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) → ((⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) → ([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)))
11	4, 8, 10	e11 45367	. . . . . . . . . 10 ⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
12	11	gen11 45295	. . . . . . . . 9 ⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑤([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
13		exbi 1875	. . . . . . . . 9 ⊢ (∀𝑤([𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) → (∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵))
14	12, 13	e1a 45306	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝑉   ▶   (∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
15		sbcex2 3803	. . . . . . . . . . 11 ⊢ ([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵)
16	15	a1i 11	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵))
17	16	bicomd 226	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → (∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵))
18	1, 17	e1a 45306	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝑉   ▶   (∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵)   )
19		bitr3 355	. . . . . . . . 9 ⊢ ((∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵) → ((∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) → ([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)))
20	19	com12 33	. . . . . . . 8 ⊢ ((∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) → ((∃𝑤[𝐴 / 𝑥]⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵) → ([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)))
21	14, 18, 20	e11 45367	. . . . . . 7 ⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
22	21	gen11 45295	. . . . . 6 ⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑦([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
23		abbib 2830	. . . . . . 7 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} ↔ ∀𝑦([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵))
24	23	biimpri 231	. . . . . 6 ⊢ (∀𝑦([𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵) → {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵})
25	22, 24	e1a 45306	. . . . 5 ⊢ (   𝐴 ∈ 𝑉   ▶   {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}   )
26		csbab 4404	. . . . . . 7 ⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}
27	26	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵})
28	1, 27	e1a 45306	. . . . 5 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}   )
29		eqeq2 2773	. . . . . 6 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} ↔ ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}))
30	29	biimpd 232	. . . . 5 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} → ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}))
31	25, 28, 30	e11 45367	. . . 4 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}   )
32		dfrn3 5879	. . . . . 6 ⊢ ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}
33	32	ax-gen 1823	. . . . 5 ⊢ ∀𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}
34		csbeq2 3857	. . . . . 6 ⊢ (∀𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} → ⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵})
35	34	a1i 11	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} → ⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}))
36	1, 33, 35	e10 45373	. . . 4 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}   )
37		eqeq2 2773	. . . . 5 ⊢ (⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} ↔ ⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}))
38	37	biimpd 232	. . . 4 ⊢ (⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵} → ⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}))
39	31, 36, 38	e11 45367	. . 3 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}   )
40		dfrn3 5879	. . 3 ⊢ ran ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}
41		eqeq2 2773	. . . 4 ⊢ (ran ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵 ↔ ⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}))
42	41	biimprcd 253	. . 3 ⊢ (⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} → (ran ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵} → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵))
43	39, 40, 42	e10 45373	. 2 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵   )
44	43	in1 45250	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1566   = wceq 1568  ∃wex 1807   ∈ wcel 2141  {cab 2739  [wsbc 3743  ⦋csb 3852  ⟨cop 4594  ran crn 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-cnv 5669  df-dm 5671  df-rn 5672  df-vd1 45249

This theorem is referenced by: (None)