Metamath Proof Explorer

Theorem bj-sbsb

Description: Biconditional showing two possible (dual) definitions of substitution df-sb not using dummy variables. (Contributed by BJ, 19-Mar-2021)

Ref Expression
Assertion bj-sbsb ( ( ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∨ ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) → ( 𝑥 = 𝑦 → 𝜑 ) )
2 pm2.27 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 = 𝑦 → 𝜑 ) → 𝜑 ) )
3 2 anc2li ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 = 𝑦 → 𝜑 ) → ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
4 3 sps ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝑥 = 𝑦 → 𝜑 ) → ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
5 olc ⊢ ( ( 𝑥 = 𝑦 ∧ 𝜑 ) → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∨ ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
6 1 4 5 syl56 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∨ ( 𝑥 = 𝑦 ∧ 𝜑 ) ) ) )
7 simpr ⊢ ( ( ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) → ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
8 equs5 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
9 8 biimpd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
10 orc ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∨ ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
11 7 9 10 syl56 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ( ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∨ ( 𝑥 = 𝑦 ∧ 𝜑 ) ) ) )
12 6 11 pm2.61i ⊢ ( ( ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∨ ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
13 sp ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ( 𝑥 = 𝑦 → 𝜑 ) )
14 pm3.4 ⊢ ( ( 𝑥 = 𝑦 ∧ 𝜑 ) → ( 𝑥 = 𝑦 → 𝜑 ) )
15 13 14 jaoi ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∨ ( 𝑥 = 𝑦 ∧ 𝜑 ) ) → ( 𝑥 = 𝑦 → 𝜑 ) )
16 equs4 ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
17 19.8a ⊢ ( ( 𝑥 = 𝑦 ∧ 𝜑 ) → ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
18 16 17 jaoi ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∨ ( 𝑥 = 𝑦 ∧ 𝜑 ) ) → ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
19 15 18 jca ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∨ ( 𝑥 = 𝑦 ∧ 𝜑 ) ) → ( ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
20 12 19 impbii ⊢ ( ( ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∨ ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )