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

Metamath Proof Explorer

Theorem onfrALTlem4

Description: Lemma for onfrALT . (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion onfrALTlem4 ( [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) ↔ ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 sbcan ⊢ ( [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) ↔ ( [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝑎 ∧ [ 𝑦 / 𝑥 ] ( 𝑎 ∩ 𝑥 ) = ∅ ) )
2 sbcel1v ⊢ ( [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎 )
3 vex ⊢ 𝑦 ∈ V
4 sbceqg ⊢ ( 𝑦 ∈ V → ( [ 𝑦 / 𝑥 ] ( 𝑎 ∩ 𝑥 ) = ∅ ↔ ⦋ 𝑦 / 𝑥 ⦌ ( 𝑎 ∩ 𝑥 ) = ⦋ 𝑦 / 𝑥 ⦌ ∅ ) )
5 3 4 ax-mp ⊢ ( [ 𝑦 / 𝑥 ] ( 𝑎 ∩ 𝑥 ) = ∅ ↔ ⦋ 𝑦 / 𝑥 ⦌ ( 𝑎 ∩ 𝑥 ) = ⦋ 𝑦 / 𝑥 ⦌ ∅ )
6 csbin ⊢ ⦋ 𝑦 / 𝑥 ⦌ ( 𝑎 ∩ 𝑥 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝑎 ∩ ⦋ 𝑦 / 𝑥 ⦌ 𝑥 )
7 csbconstg ⊢ ( 𝑦 ∈ V → ⦋ 𝑦 / 𝑥 ⦌ 𝑎 = 𝑎 )
8 3 7 ax-mp ⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝑎 = 𝑎
9 csbvarg ⊢ ( 𝑦 ∈ V → ⦋ 𝑦 / 𝑥 ⦌ 𝑥 = 𝑦 )
10 3 9 ax-mp ⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝑥 = 𝑦
11 8 10 ineq12i ⊢ ( ⦋ 𝑦 / 𝑥 ⦌ 𝑎 ∩ ⦋ 𝑦 / 𝑥 ⦌ 𝑥 ) = ( 𝑎 ∩ 𝑦 )
12 6 11 eqtri ⊢ ⦋ 𝑦 / 𝑥 ⦌ ( 𝑎 ∩ 𝑥 ) = ( 𝑎 ∩ 𝑦 )
13 csb0 ⊢ ⦋ 𝑦 / 𝑥 ⦌ ∅ = ∅
14 12 13 eqeq12i ⊢ ( ⦋ 𝑦 / 𝑥 ⦌ ( 𝑎 ∩ 𝑥 ) = ⦋ 𝑦 / 𝑥 ⦌ ∅ ↔ ( 𝑎 ∩ 𝑦 ) = ∅ )
15 5 14 bitri ⊢ ( [ 𝑦 / 𝑥 ] ( 𝑎 ∩ 𝑥 ) = ∅ ↔ ( 𝑎 ∩ 𝑦 ) = ∅ )
16 2 15 anbi12i ⊢ ( ( [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝑎 ∧ [ 𝑦 / 𝑥 ] ( 𝑎 ∩ 𝑥 ) = ∅ ) ↔ ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) )
17 1 16 bitri ⊢ ( [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) ↔ ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) )