ss2abdv

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011) Avoid ax-8 , ax-10 , ax-11 , ax-12 . (Revised by Gino Giotto, 28-Jun-2024)

		Ref	Expression
	Hypothesis	ss2abdv.1	$⊢ φ \to (ψ \to χ)$
	Assertion	ss2abdv	$⊢ φ \to \{x \| ψ\} \subseteq \{x \| χ\}$

Proof

Step	Hyp	Ref	Expression
1		ss2abdv.1	$⊢ φ \to (ψ \to χ)$
2		df-in	$⊢ \{x \| ψ\} \cap \{x \| χ\} = \{y \| (y \in \{x \| ψ\} \land y \in \{x \| χ\})\}$
3		df-clab	$⊢ y \in \{x \| ψ\} \leftrightarrow [y/ x] ψ$
4	3	bicomi	$⊢ [y/ x] ψ \leftrightarrow y \in \{x \| ψ\}$
5		df-clab	$⊢ y \in \{x \| χ\} \leftrightarrow [y/ x] χ$
6	5	bicomi	$⊢ [y/ x] χ \leftrightarrow y \in \{x \| χ\}$
7	4 6	anbi12i	$⊢ ([y/ x] ψ \land [y/ x] χ) \leftrightarrow (y \in \{x \| ψ\} \land y \in \{x \| χ\})$
8	7	abbii	$⊢ \{y \| ([y/ x] ψ \land [y/ x] χ)\} = \{y \| (y \in \{x \| ψ\} \land y \in \{x \| χ\})\}$
9		sbequ	$⊢ y = z \to ([y/ x] ψ \leftrightarrow [z/ x] ψ)$
10		sbequ	$⊢ y = z \to ([y/ x] χ \leftrightarrow [z/ x] χ)$
11	9 10	anbi12d	$⊢ y = z \to (([y/ x] ψ \land [y/ x] χ) \leftrightarrow ([z/ x] ψ \land [z/ x] χ))$
12	11	sbievw	$⊢ [z/ y] ([y/ x] ψ \land [y/ x] χ) \leftrightarrow ([z/ x] ψ \land [z/ x] χ)$
13		ax-1	$⊢ [z/ x] ψ \to ([z/ x] χ \to [z/ x] ψ)$
14	13	a1i	$⊢ φ \to ([z/ x] ψ \to ([z/ x] χ \to [z/ x] ψ))$
15	14	impd	$⊢ φ \to (([z/ x] ψ \land [z/ x] χ) \to [z/ x] ψ)$
16	1	sbimdv	$⊢ φ \to ([z/ x] ψ \to [z/ x] χ)$
17	16	ancld	$⊢ φ \to ([z/ x] ψ \to ([z/ x] ψ \land [z/ x] χ))$
18	15 17	impbid	$⊢ φ \to (([z/ x] ψ \land [z/ x] χ) \leftrightarrow [z/ x] ψ)$
19	12 18	bitrid	$⊢ φ \to ([z/ y] ([y/ x] ψ \land [y/ x] χ) \leftrightarrow [z/ x] ψ)$
20		df-clab	$⊢ z \in \{y \| ([y/ x] ψ \land [y/ x] χ)\} \leftrightarrow [z/ y] ([y/ x] ψ \land [y/ x] χ)$
21		df-clab	$⊢ z \in \{x \| ψ\} \leftrightarrow [z/ x] ψ$
22	19 20 21	3bitr4g	$⊢ φ \to (z \in \{y \| ([y/ x] ψ \land [y/ x] χ)\} \leftrightarrow z \in \{x \| ψ\})$
23	22	eqrdv	$⊢ φ \to \{y \| ([y/ x] ψ \land [y/ x] χ)\} = \{x \| ψ\}$
24	8 23	eqtr3id	$⊢ φ \to \{y \| (y \in \{x \| ψ\} \land y \in \{x \| χ\})\} = \{x \| ψ\}$
25	2 24	eqtrid	$⊢ φ \to \{x \| ψ\} \cap \{x \| χ\} = \{x \| ψ\}$
26		df-ss	$⊢ \{x \| ψ\} \subseteq \{x \| χ\} \leftrightarrow \{x \| ψ\} \cap \{x \| χ\} = \{x \| ψ\}$
27	25 26	sylibr	$⊢ φ \to \{x \| ψ\} \subseteq \{x \| χ\}$

Metamath Proof Explorer

Theorem ss2abdv

Proof