This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rspct

Description: A closed version of rspc . (Contributed by Andrew Salmon, 6-Jun-2011)

Ref Expression
Hypothesis rspct.1 ⊢ Ⅎ 𝑥 𝜓
Assertion rspct ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝜑 → 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 rspct.1 ⊢ Ⅎ 𝑥 𝜓
2 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜑 ) )
3 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
4 3 adantr ⊢ ( ( 𝑥 = 𝐴 ∧ ( 𝜑 ↔ 𝜓 ) ) → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
5 simpr ⊢ ( ( 𝑥 = 𝐴 ∧ ( 𝜑 ↔ 𝜓 ) ) → ( 𝜑 ↔ 𝜓 ) )
6 4 5 imbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ ( 𝜑 ↔ 𝜓 ) ) → ( ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → 𝜓 ) ) )
7 6 ex ⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → 𝜓 ) ) ) )
8 7 a2i ⊢ ( ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → 𝜓 ) ) ) )
9 8 alimi ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ∀ 𝑥 ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → 𝜓 ) ) ) )
10 nfv ⊢ Ⅎ 𝑥 𝐴 ∈ 𝐵
11 10 1 nfim ⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝐵 → 𝜓 )
12 nfcv ⊢ Ⅎ 𝑥 𝐴
13 11 12 spcgft ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → 𝜓 ) ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝐴 ∈ 𝐵 → 𝜓 ) ) ) )
14 9 13 syl ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝐴 ∈ 𝐵 → 𝜓 ) ) ) )
15 2 14 syl7bi ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝜑 → ( 𝐴 ∈ 𝐵 → 𝜓 ) ) ) )
16 15 com34 ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝜑 → 𝜓 ) ) ) )
17 16 pm2.43d ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝜑 → 𝜓 ) ) )