Theorem ralrnmpt 7087

Description: A restricted quantifier over an image set. Usage of this theorem is discouraged because it depends on ax-13 2363. Use the weaker ralrnmptw 7085 when possible. (Contributed by Mario Carneiro, 20-Aug-2015.) (New usage is discouraged.)

Hypotheses

Ref	Expression
ralrnmpt.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
ralrnmpt.2	⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
ralrnmpt	⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable groups:   𝑥,𝐴   𝑦,𝐵   𝜒,𝑦   𝑦,𝐹   𝜓,𝑥

Allowed substitution hints:   𝜓(𝑦)   𝜒(𝑥)   𝐴(𝑦)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥,𝑦)

Proof of Theorem ralrnmpt

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

Step	Hyp	Ref	Expression
1		ralrnmpt.1	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	fnmpt 6680	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴)
3		dfsbcq 3771	. . . . 5 ⊢ (𝑤 = (𝐹‘𝑧) → ([𝑤 / 𝑦]𝜓 ↔ [(𝐹‘𝑧) / 𝑦]𝜓))
4	3	ralrn 7079	. . . 4 ⊢ (𝐹 Fn 𝐴 → (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓))
5	2, 4	syl 17	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓))
6		nfv 1909	. . . . 5 ⊢ Ⅎ𝑤𝜓
7		nfsbc1v 3789	. . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜓
8		sbceq1a 3780	. . . . 5 ⊢ (𝑦 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑦]𝜓))
9	6, 7, 8	cbvral 3350	. . . 4 ⊢ (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓)
10	9	bicomi 223	. . 3 ⊢ (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑦 ∈ ran 𝐹𝜓)
11		nfmpt1 5246	. . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
12	1, 11	nfcxfr 2893	. . . . . 6 ⊢ Ⅎ𝑥𝐹
13		nfcv 2895	. . . . . 6 ⊢ Ⅎ𝑥𝑧
14	12, 13	nffv 6891	. . . . 5 ⊢ Ⅎ𝑥(𝐹‘𝑧)
15		nfv 1909	. . . . 5 ⊢ Ⅎ𝑥𝜓
16	14, 15	nfsbc 3794	. . . 4 ⊢ Ⅎ𝑥[(𝐹‘𝑧) / 𝑦]𝜓
17		nfv 1909	. . . 4 ⊢ Ⅎ𝑧[(𝐹‘𝑥) / 𝑦]𝜓
18		fveq2 6881	. . . . 5 ⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥))
19	18	sbceq1d 3774	. . . 4 ⊢ (𝑧 = 𝑥 → ([(𝐹‘𝑧) / 𝑦]𝜓 ↔ [(𝐹‘𝑥) / 𝑦]𝜓))
20	16, 17, 19	cbvral 3350	. . 3 ⊢ (∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓)
21	5, 10, 20	3bitr3g 313	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓))
22	1	fvmpt2 6999	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → (𝐹‘𝑥) = 𝐵)
23	22	sbceq1d 3774	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ [𝐵 / 𝑦]𝜓))
24		ralrnmpt.2	. . . . . . 7 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
25	24	sbcieg 3809	. . . . . 6 ⊢ (𝐵 ∈ 𝑉 → ([𝐵 / 𝑦]𝜓 ↔ 𝜒))
26	25	adantl 481	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([𝐵 / 𝑦]𝜓 ↔ 𝜒))
27	23, 26	bitrd 279	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒))
28	27	ralimiaa 3074	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒))
29		ralbi 3095	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒) → (∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
30	28, 29	syl 17	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
31	21, 30	bitrd 279	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  ∀wral 3053  [wsbc 3769   ↦ cmpt 5221  ran crn 5667   Fn wfn 6528  ‘cfv 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-13 2363  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-fv 6541

This theorem is referenced by:  rexrnmpt  7088