Theorem ralrnmpt2 5534

Description: A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)

Hypotheses

Ref	Expression
rngop.1	⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)
ralrnmpt2.2	⊢ (z = 𝐶 → (φ ↔ ψ))

Assertion

Ref	Expression
ralrnmpt2	⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝑉 → (∀z ∈ ran 𝐹φ ↔ ∀x ∈ A ∀y ∈ B ψ))

Distinct variable groups:   y,z,A   z,B   z,𝐶   z,𝐹   ψ,z   x,y,z   φ,x,y

Allowed substitution hints:   φ(z)   ψ(x,y)   A(x)   B(x,y)   𝐶(x,y)   𝐹(x,y)   𝑉(x,y,z)

Proof of Theorem ralrnmpt2

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rngop.1	. . . . 5 ⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)
2	1	rnmpt2 5530	. . . 4 ⊢ ran 𝐹 = {w ∣ ∃x ∈ A ∃y ∈ B w = 𝐶}
3	2	raleqi 2483	. . 3 ⊢ (∀z ∈ ran 𝐹φ ↔ ∀z ∈ {w ∣ ∃x ∈ A ∃y ∈ B w = 𝐶}φ)
4		eqeq1 2024	. . . . 5 ⊢ (w = z → (w = 𝐶 ↔ z = 𝐶))
5	4	2rexbidv 2323	. . . 4 ⊢ (w = z → (∃x ∈ A ∃y ∈ B w = 𝐶 ↔ ∃x ∈ A ∃y ∈ B z = 𝐶))
6	5	ralab 2674	. . 3 ⊢ (∀z ∈ {w ∣ ∃x ∈ A ∃y ∈ B w = 𝐶}φ ↔ ∀z(∃x ∈ A ∃y ∈ B z = 𝐶 → φ))
7		ralcom4 2549	. . . 4 ⊢ (∀x ∈ A ∀z(∃y ∈ B z = 𝐶 → φ) ↔ ∀z∀x ∈ A (∃y ∈ B z = 𝐶 → φ))
8		r19.23v 2399	. . . . 5 ⊢ (∀x ∈ A (∃y ∈ B z = 𝐶 → φ) ↔ (∃x ∈ A ∃y ∈ B z = 𝐶 → φ))
9	8	albii 1335	. . . 4 ⊢ (∀z∀x ∈ A (∃y ∈ B z = 𝐶 → φ) ↔ ∀z(∃x ∈ A ∃y ∈ B z = 𝐶 → φ))
10	7, 9	bitr2i 174	. . 3 ⊢ (∀z(∃x ∈ A ∃y ∈ B z = 𝐶 → φ) ↔ ∀x ∈ A ∀z(∃y ∈ B z = 𝐶 → φ))
11	3, 6, 10	3bitri 195	. 2 ⊢ (∀z ∈ ran 𝐹φ ↔ ∀x ∈ A ∀z(∃y ∈ B z = 𝐶 → φ))
12		ralcom4 2549	. . . . . 6 ⊢ (∀y ∈ B ∀z(z = 𝐶 → φ) ↔ ∀z∀y ∈ B (z = 𝐶 → φ))
13		r19.23v 2399	. . . . . . 7 ⊢ (∀y ∈ B (z = 𝐶 → φ) ↔ (∃y ∈ B z = 𝐶 → φ))
14	13	albii 1335	. . . . . 6 ⊢ (∀z∀y ∈ B (z = 𝐶 → φ) ↔ ∀z(∃y ∈ B z = 𝐶 → φ))
15	12, 14	bitri 173	. . . . 5 ⊢ (∀y ∈ B ∀z(z = 𝐶 → φ) ↔ ∀z(∃y ∈ B z = 𝐶 → φ))
16		nfv 1398	. . . . . . . 8 ⊢ Ⅎzψ
17		ralrnmpt2.2	. . . . . . . 8 ⊢ (z = 𝐶 → (φ ↔ ψ))
18	16, 17	ceqsalg 2555	. . . . . . 7 ⊢ (𝐶 ∈ 𝑉 → (∀z(z = 𝐶 → φ) ↔ ψ))
19	18	ralimi 2358	. . . . . 6 ⊢ (∀y ∈ B 𝐶 ∈ 𝑉 → ∀y ∈ B (∀z(z = 𝐶 → φ) ↔ ψ))
20		ralbi 2419	. . . . . 6 ⊢ (∀y ∈ B (∀z(z = 𝐶 → φ) ↔ ψ) → (∀y ∈ B ∀z(z = 𝐶 → φ) ↔ ∀y ∈ B ψ))
21	19, 20	syl 14	. . . . 5 ⊢ (∀y ∈ B 𝐶 ∈ 𝑉 → (∀y ∈ B ∀z(z = 𝐶 → φ) ↔ ∀y ∈ B ψ))
22	15, 21	syl5bbr 183	. . . 4 ⊢ (∀y ∈ B 𝐶 ∈ 𝑉 → (∀z(∃y ∈ B z = 𝐶 → φ) ↔ ∀y ∈ B ψ))
23	22	ralimi 2358	. . 3 ⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝑉 → ∀x ∈ A (∀z(∃y ∈ B z = 𝐶 → φ) ↔ ∀y ∈ B ψ))
24		ralbi 2419	. . 3 ⊢ (∀x ∈ A (∀z(∃y ∈ B z = 𝐶 → φ) ↔ ∀y ∈ B ψ) → (∀x ∈ A ∀z(∃y ∈ B z = 𝐶 → φ) ↔ ∀x ∈ A ∀y ∈ B ψ))
25	23, 24	syl 14	. 2 ⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝑉 → (∀x ∈ A ∀z(∃y ∈ B z = 𝐶 → φ) ↔ ∀x ∈ A ∀y ∈ B ψ))
26	11, 25	syl5bb 181	1 ⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝑉 → (∀z ∈ ran 𝐹φ ↔ ∀x ∈ A ∀y ∈ B ψ))

Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1224   = wceq 1226   ∈ wcel 1370  {cab 2004  ∀wral 2280  ∃wrex 2281  ran crn 4269   ↦ cmpt2 5434

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-br 3735  df-opab 3789  df-cnv 4276  df-dm 4278  df-rn 4279  df-oprab 5436  df-mpt2 5437

This theorem is referenced by: (None)