Metamath Proof Explorer

Theorem rspcsbnea

Description: Special case related to rspsbc . (Contributed by metakunt, 5-May-2025)

Ref Expression
Assertion rspcsbnea ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 𝐶 ≠ 𝐷 ) → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ≠ 𝐷 )

Proof

Step Hyp Ref Expression
1 rspsbc ⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝐶 ≠ 𝐷 → [ 𝐴 / 𝑥 ] 𝐶 ≠ 𝐷 ) )
2 df-ne ⊢ ( 𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷 )
3 2 sbcbii ⊢ ( [ 𝐴 / 𝑥 ] 𝐶 ≠ 𝐷 ↔ [ 𝐴 / 𝑥 ] ¬ 𝐶 = 𝐷 )
4 3 a1i ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝐶 ≠ 𝐷 ↔ [ 𝐴 / 𝑥 ] ¬ 𝐶 = 𝐷 ) )
5 sbcng ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ¬ 𝐶 = 𝐷 ↔ ¬ [ 𝐴 / 𝑥 ] 𝐶 = 𝐷 ) )
6 sbceq1g ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝐶 = 𝐷 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = 𝐷 ) )
7 6 notbid ⊢ ( 𝐴 ∈ 𝐵 → ( ¬ [ 𝐴 / 𝑥 ] 𝐶 = 𝐷 ↔ ¬ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = 𝐷 ) )
8 5 7 bitrd ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ¬ 𝐶 = 𝐷 ↔ ¬ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = 𝐷 ) )
9 4 8 bitrd ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝐶 ≠ 𝐷 ↔ ¬ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = 𝐷 ) )
10 biidd ⊢ ( 𝐴 ∈ 𝐵 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = 𝐷 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = 𝐷 ) )
11 10 necon3bbid ⊢ ( 𝐴 ∈ 𝐵 → ( ¬ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = 𝐷 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ≠ 𝐷 ) )
12 9 11 bitrd ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝐶 ≠ 𝐷 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ≠ 𝐷 ) )
13 1 12 sylibd ⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝐶 ≠ 𝐷 → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ≠ 𝐷 ) )
14 13 imp ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 𝐶 ≠ 𝐷 ) → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ≠ 𝐷 )