Theorem ralrnmpt2 5557

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 5553	. . . 4 ⊢ ran 𝐹 = {w ∣ ∃x ∈ A ∃y ∈ B w = 𝐶}
3	2	raleqi 2503	. . 3 ⊢ (∀z ∈ ran 𝐹φ ↔ ∀z ∈ {w ∣ ∃x ∈ A ∃y ∈ B w = 𝐶}φ)
4		eqeq1 2043	. . . . 5 ⊢ (w = z → (w = 𝐶 ↔ z = 𝐶))
5	4	2rexbidv 2343	. . . 4 ⊢ (w = z → (∃x ∈ A ∃y ∈ B w = 𝐶 ↔ ∃x ∈ A ∃y ∈ B z = 𝐶))
6	5	ralab 2695	. . 3 ⊢ (∀z ∈ {w ∣ ∃x ∈ A ∃y ∈ B w = 𝐶}φ ↔ ∀z(∃x ∈ A ∃y ∈ B z = 𝐶 → φ))
7		ralcom4 2570	. . . 4 ⊢ (∀x ∈ A ∀z(∃y ∈ B z = 𝐶 → φ) ↔ ∀z∀x ∈ A (∃y ∈ B z = 𝐶 → φ))
8		r19.23v 2419	. . . . 5 ⊢ (∀x ∈ A (∃y ∈ B z = 𝐶 → φ) ↔ (∃x ∈ A ∃y ∈ B z = 𝐶 → φ))
9	8	albii 1356	. . . 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 2570	. . . . . 6 ⊢ (∀y ∈ B ∀z(z = 𝐶 → φ) ↔ ∀z∀y ∈ B (z = 𝐶 → φ))
13		r19.23v 2419	. . . . . . 7 ⊢ (∀y ∈ B (z = 𝐶 → φ) ↔ (∃y ∈ B z = 𝐶 → φ))
14	13	albii 1356	. . . . . 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 1418	. . . . . . . 8 ⊢ Ⅎzψ
17		ralrnmpt2.2	. . . . . . . 8 ⊢ (z = 𝐶 → (φ ↔ ψ))
18	16, 17	ceqsalg 2576	. . . . . . 7 ⊢ (𝐶 ∈ 𝑉 → (∀z(z = 𝐶 → φ) ↔ ψ))
19	18	ralimi 2378	. . . . . 6 ⊢ (∀y ∈ B 𝐶 ∈ 𝑉 → ∀y ∈ B (∀z(z = 𝐶 → φ) ↔ ψ))
20		ralbi 2439	. . . . . 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 2378	. . 3 ⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝑉 → ∀x ∈ A (∀z(∃y ∈ B z = 𝐶 → φ) ↔ ∀y ∈ B ψ))
24		ralbi 2439	. . 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 1240   = wceq 1242   ∈ wcel 1390  {cab 2023  ∀wral 2300  ∃wrex 2301  ran crn 4289   ↦ cmpt2 5457

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-cnv 4296  df-dm 4298  df-rn 4299  df-oprab 5459  df-mpt2 5460

This theorem is referenced by: (None)