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	$⊢ ((x = y \to φ) \land \exists x (x = y \land φ)) \leftrightarrow (\forall x (x = y \to φ) \lor (x = y \land φ))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ ((x = y \to φ) \land \exists x (x = y \land φ)) \to (x = y \to φ)$
2		pm2.27	$⊢ x = y \to ((x = y \to φ) \to φ)$
3	2	anc2li	$⊢ x = y \to ((x = y \to φ) \to (x = y \land φ))$
4	3	sps	$⊢ \forall x x = y \to ((x = y \to φ) \to (x = y \land φ))$
5		olc	$⊢ (x = y \land φ) \to (\forall x (x = y \to φ) \lor (x = y \land φ))$
6	1 4 5	syl56	$⊢ \forall x x = y \to (((x = y \to φ) \land \exists x (x = y \land φ)) \to (\forall x (x = y \to φ) \lor (x = y \land φ)))$
7		simpr	$⊢ ((x = y \to φ) \land \exists x (x = y \land φ)) \to \exists x (x = y \land φ)$
8		equs5	$⊢ \neg \forall x x = y \to (\exists x (x = y \land φ) \leftrightarrow \forall x (x = y \to φ))$
9	8	biimpd	$⊢ \neg \forall x x = y \to (\exists x (x = y \land φ) \to \forall x (x = y \to φ))$
10		orc	$⊢ \forall x (x = y \to φ) \to (\forall x (x = y \to φ) \lor (x = y \land φ))$
11	7 9 10	syl56	$⊢ \neg \forall x x = y \to (((x = y \to φ) \land \exists x (x = y \land φ)) \to (\forall x (x = y \to φ) \lor (x = y \land φ)))$
12	6 11	pm2.61i	$⊢ ((x = y \to φ) \land \exists x (x = y \land φ)) \to (\forall x (x = y \to φ) \lor (x = y \land φ))$
13		sp	$⊢ \forall x (x = y \to φ) \to (x = y \to φ)$
14		pm3.4	$⊢ (x = y \land φ) \to (x = y \to φ)$
15	13 14	jaoi	$⊢ (\forall x (x = y \to φ) \lor (x = y \land φ)) \to (x = y \to φ)$
16		equs4	$⊢ \forall x (x = y \to φ) \to \exists x (x = y \land φ)$
17		19.8a	$⊢ (x = y \land φ) \to \exists x (x = y \land φ)$
18	16 17	jaoi	$⊢ (\forall x (x = y \to φ) \lor (x = y \land φ)) \to \exists x (x = y \land φ)$
19	15 18	jca	$⊢ (\forall x (x = y \to φ) \lor (x = y \land φ)) \to ((x = y \to φ) \land \exists x (x = y \land φ))$
20	12 19	impbii	$⊢ ((x = y \to φ) \land \exists x (x = y \land φ)) \leftrightarrow (\forall x (x = y \to φ) \lor (x = y \land φ))$

Metamath Proof Explorer

Theorem bj-sbsb

Proof