Metamath Proof Explorer

Theorem ralrnmptw

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

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

Proof

Step Hyp Ref Expression
1 ralrnmptw.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2 ralrnmptw.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
3 1 fnmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴 )
4 dfsbcq ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑧 ) → ( [ 𝑤 / 𝑦 ] 𝜓 ↔ [ ( 𝐹 ‘ 𝑧 ) / 𝑦 ] 𝜓 ) )
5 4 ralrn ⊢ ( 𝐹 Fn 𝐴 → ( ∀ 𝑤 ∈ ran 𝐹 [ 𝑤 / 𝑦 ] 𝜓 ↔ ∀ 𝑧 ∈ 𝐴 [ ( 𝐹 ‘ 𝑧 ) / 𝑦 ] 𝜓 ) )
6 3 5 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( ∀ 𝑤 ∈ ran 𝐹 [ 𝑤 / 𝑦 ] 𝜓 ↔ ∀ 𝑧 ∈ 𝐴 [ ( 𝐹 ‘ 𝑧 ) / 𝑦 ] 𝜓 ) )
7 nfsbc1v ⊢ Ⅎ 𝑦 [ 𝑤 / 𝑦 ] 𝜓
8 nfv ⊢ Ⅎ 𝑤 𝜓
9 sbceq2a ⊢ ( 𝑤 = 𝑦 → ( [ 𝑤 / 𝑦 ] 𝜓 ↔ 𝜓 ) )
10 7 8 9 cbvralw ⊢ ( ∀ 𝑤 ∈ ran 𝐹 [ 𝑤 / 𝑦 ] 𝜓 ↔ ∀ 𝑦 ∈ ran 𝐹 𝜓 )
11 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
12 1 11 nfcxfr ⊢ Ⅎ 𝑥 𝐹
13 nfcv ⊢ Ⅎ 𝑥 𝑧
14 12 13 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 )
15 nfv ⊢ Ⅎ 𝑥 𝜓
16 14 15 nfsbcw ⊢ Ⅎ 𝑥 [ ( 𝐹 ‘ 𝑧 ) / 𝑦 ] 𝜓
17 nfv ⊢ Ⅎ 𝑧 [ ( 𝐹 ‘ 𝑥 ) / 𝑦 ] 𝜓
18 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
19 18 sbceq1d ⊢ ( 𝑧 = 𝑥 → ( [ ( 𝐹 ‘ 𝑧 ) / 𝑦 ] 𝜓 ↔ [ ( 𝐹 ‘ 𝑥 ) / 𝑦 ] 𝜓 ) )
20 16 17 19 cbvralw ⊢ ( ∀ 𝑧 ∈ 𝐴 [ ( 𝐹 ‘ 𝑧 ) / 𝑦 ] 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 [ ( 𝐹 ‘ 𝑥 ) / 𝑦 ] 𝜓 )
21 6 10 20 3bitr3g ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( ∀ 𝑦 ∈ ran 𝐹 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 [ ( 𝐹 ‘ 𝑥 ) / 𝑦 ] 𝜓 ) )
22 1 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
23 22 sbceq1d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( [ ( 𝐹 ‘ 𝑥 ) / 𝑦 ] 𝜓 ↔ [ 𝐵 / 𝑦 ] 𝜓 ) )
24 2 sbcieg ⊢ ( 𝐵 ∈ 𝑉 → ( [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜒 ) )
25 24 adantl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜒 ) )
26 23 25 bitrd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( [ ( 𝐹 ‘ 𝑥 ) / 𝑦 ] 𝜓 ↔ 𝜒 ) )
27 26 ralimiaa ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 ( [ ( 𝐹 ‘ 𝑥 ) / 𝑦 ] 𝜓 ↔ 𝜒 ) )
28 ralbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( [ ( 𝐹 ‘ 𝑥 ) / 𝑦 ] 𝜓 ↔ 𝜒 ) → ( ∀ 𝑥 ∈ 𝐴 [ ( 𝐹 ‘ 𝑥 ) / 𝑦 ] 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
29 27 28 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 [ ( 𝐹 ‘ 𝑥 ) / 𝑦 ] 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
30 21 29 bitrd ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( ∀ 𝑦 ∈ ran 𝐹 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 𝜒 ) )