ceqsralbv

Description: Elimination of a restricted universal quantifier, using implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020)

		Ref	Expression
	Hypothesis	ceqsrexv.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
	Assertion	ceqsralbv	$⊢ \forall x \in B (x = A \to φ) \leftrightarrow (A \in B \to ψ)$

Step	Hyp	Ref	Expression
1		ceqsrexv.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2	1	notbid	$⊢ x = A \to (\neg φ \leftrightarrow \neg ψ)$
3	2	ceqsrexbv	$⊢ \exists x \in B (x = A \land \neg φ) \leftrightarrow (A \in B \land \neg ψ)$
4		rexanali	$⊢ \exists x \in B (x = A \land \neg φ) \leftrightarrow \neg \forall x \in B (x = A \to φ)$
5		annim	$⊢ (A \in B \land \neg ψ) \leftrightarrow \neg (A \in B \to ψ)$
6	3 4 5	3bitr3i	$⊢ \neg \forall x \in B (x = A \to φ) \leftrightarrow \neg (A \in B \to ψ)$
7	6	con4bii	$⊢ \forall x \in B (x = A \to φ) \leftrightarrow (A \in B \to ψ)$

Metamath Proof Explorer