Theorem subsym1

Description: A symmetry with [ x / y ] .

See negsym1 for more information. (Contributed by Anthony Hart, 11-Sep-2011)

	Ref	Expression
Assertion	subsym1	⊢ ( [ 𝑦 / 𝑥 ] [ 𝑦 / 𝑥 ] ⊥ → [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		fal	⊢ ¬ ⊥
2	1	intnan	⊢ ¬ ( 𝑥 = 𝑦 ∧ ⊥ )
3	2	nex	⊢ ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ ⊥ )
4	3	intnan	⊢ ¬ ( ( 𝑥 = 𝑦 → ⊥ ) ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ ⊥ ) )
5		dfsb1	⊢ ( [ 𝑦 / 𝑥 ] ⊥ ↔ ( ( 𝑥 = 𝑦 → ⊥ ) ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ ⊥ ) ) )
6	4 5	mtbir	⊢ ¬ [ 𝑦 / 𝑥 ] ⊥
7	6	intnan	⊢ ¬ ( 𝑥 = 𝑦 ∧ [ 𝑦 / 𝑥 ] ⊥ )
8	7	nex	⊢ ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ [ 𝑦 / 𝑥 ] ⊥ )
9	8	intnan	⊢ ¬ ( ( 𝑥 = 𝑦 → [ 𝑦 / 𝑥 ] ⊥ ) ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ [ 𝑦 / 𝑥 ] ⊥ ) )
10		dfsb1	⊢ ( [ 𝑦 / 𝑥 ] [ 𝑦 / 𝑥 ] ⊥ ↔ ( ( 𝑥 = 𝑦 → [ 𝑦 / 𝑥 ] ⊥ ) ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ [ 𝑦 / 𝑥 ] ⊥ ) ) )
11	9 10	mtbir	⊢ ¬ [ 𝑦 / 𝑥 ] [ 𝑦 / 𝑥 ] ⊥
12	11	pm2.21i	⊢ ( [ 𝑦 / 𝑥 ] [ 𝑦 / 𝑥 ] ⊥ → [ 𝑦 / 𝑥 ] 𝜑 )