Metamath Proof Explorer

Theorem ralrnmpt

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

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

Proof

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