Theorem ralrnmptw 7114

Description: A restricted quantifier over an image set. Version of ralrnmpt 7116 with a disjoint variable condition, which does not require ax-13 2375. (Contributed by Mario Carneiro, 20-Aug-2015.) Avoid ax-13 2375. (Revised by GG, 26-Jan-2024.)

Hypotheses

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

Assertion

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

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

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

Proof of Theorem ralrnmptw

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

Step	Hyp	Ref	Expression
1		ralrnmptw.1	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	fnmpt 6709	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴)
3		dfsbcq 3793	. . . . 5 ⊢ (𝑤 = (𝐹‘𝑧) → ([𝑤 / 𝑦]𝜓 ↔ [(𝐹‘𝑧) / 𝑦]𝜓))
4	3	ralrn 7108	. . . 4 ⊢ (𝐹 Fn 𝐴 → (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓))
5	2, 4	syl 17	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓))
6		nfsbc1v 3811	. . . 4 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜓
7		nfv 1912	. . . 4 ⊢ Ⅎ𝑤𝜓
8		sbceq2a 3803	. . . 4 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑦]𝜓 ↔ 𝜓))
9	6, 7, 8	cbvralw 3304	. . 3 ⊢ (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑦 ∈ ran 𝐹𝜓)
10		nfmpt1 5256	. . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
11	1, 10	nfcxfr 2901	. . . . . 6 ⊢ Ⅎ𝑥𝐹
12		nfcv 2903	. . . . . 6 ⊢ Ⅎ𝑥𝑧
13	11, 12	nffv 6917	. . . . 5 ⊢ Ⅎ𝑥(𝐹‘𝑧)
14		nfv 1912	. . . . 5 ⊢ Ⅎ𝑥𝜓
15	13, 14	nfsbcw 3813	. . . 4 ⊢ Ⅎ𝑥[(𝐹‘𝑧) / 𝑦]𝜓
16		nfv 1912	. . . 4 ⊢ Ⅎ𝑧[(𝐹‘𝑥) / 𝑦]𝜓
17		fveq2 6907	. . . . 5 ⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥))
18	17	sbceq1d 3796	. . . 4 ⊢ (𝑧 = 𝑥 → ([(𝐹‘𝑧) / 𝑦]𝜓 ↔ [(𝐹‘𝑥) / 𝑦]𝜓))
19	15, 16, 18	cbvralw 3304	. . 3 ⊢ (∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓)
20	5, 9, 19	3bitr3g 313	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓))
21	1	fvmpt2 7027	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → (𝐹‘𝑥) = 𝐵)
22	21	sbceq1d 3796	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ [𝐵 / 𝑦]𝜓))
23		ralrnmptw.2	. . . . . . 7 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
24	23	sbcieg 3832	. . . . . 6 ⊢ (𝐵 ∈ 𝑉 → ([𝐵 / 𝑦]𝜓 ↔ 𝜒))
25	24	adantl 481	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([𝐵 / 𝑦]𝜓 ↔ 𝜒))
26	22, 25	bitrd 279	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒))
27	26	ralimiaa 3080	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒))
28		ralbi 3101	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒) → (∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
29	27, 28	syl 17	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
30	20, 29	bitrd 279	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∀wral 3059  [wsbc 3791   ↦ cmpt 5231  ran crn 5690   Fn wfn 6558  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-fv 6571

This theorem is referenced by:  rexrnmptw  7115  ac6num  10517  gsumwspan  18872  dfod2  19597  ordtbaslem  23212  ordtrest2lem  23227  cncmp  23416  comppfsc  23556  ptpjopn  23636  ordthmeolem  23825  tsmsfbas  24152  tsmsf1o  24169  prdsxmetlem  24394  prdsbl  24520  metdsf  24884  metdsge  24885  minveclem1  25472  minveclem3b  25476  minveclem6  25482  mbflimsup  25715  xrlimcnp  27026  minvecolem1  30903  minvecolem5  30910  minvecolem6  30911  ordtrest2NEWlem  33883  cvmsss2  35259  fin2so  37594  prdsbnd  37780  rrnequiv  37822  ralrnmpt3  45204