eqoprab2bw

Description: Equivalence of ordered pair abstraction subclass and biconditional. Version of eqoprab2b with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 4-Jan-2017) (Revised by Gino Giotto, 26-Jan-2024)

		Ref	Expression
	Assertion	eqoprab2bw	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨⟨x, y⟩, z⟩ \| ψ\} \leftrightarrow \forall x \forall y \forall z (φ \leftrightarrow ψ)$

Proof

Step	Hyp	Ref	Expression
1		nfoprab1	$⊢ \underline{Ⅎ} x \{⟨⟨x, y⟩, z⟩ \| φ\}$
2		nfoprab1	$⊢ \underline{Ⅎ} x \{⟨⟨x, y⟩, z⟩ \| ψ\}$
3	1 2	nfss	$⊢ Ⅎ x \{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\}$
4		nfoprab2	$⊢ \underline{Ⅎ} y \{⟨⟨x, y⟩, z⟩ \| φ\}$
5		nfoprab2	$⊢ \underline{Ⅎ} y \{⟨⟨x, y⟩, z⟩ \| ψ\}$
6	4 5	nfss	$⊢ Ⅎ y \{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\}$
7		nfoprab3	$⊢ \underline{Ⅎ} z \{⟨⟨x, y⟩, z⟩ \| φ\}$
8		nfoprab3	$⊢ \underline{Ⅎ} z \{⟨⟨x, y⟩, z⟩ \| ψ\}$
9	7 8	nfss	$⊢ Ⅎ z \{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\}$
10		ssel	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\} \to (⟨⟨x, y⟩, z⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \to ⟨⟨x, y⟩, z⟩ \in \{⟨⟨x, y⟩, z⟩ \| ψ\})$
11		oprabidw	$⊢ ⟨⟨x, y⟩, z⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow φ$
12		oprabidw	$⊢ ⟨⟨x, y⟩, z⟩ \in \{⟨⟨x, y⟩, z⟩ \| ψ\} \leftrightarrow ψ$
13	10 11 12	3imtr3g	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\} \to (φ \to ψ)$
14	9 13	alrimi	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\} \to \forall z (φ \to ψ)$
15	6 14	alrimi	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\} \to \forall y \forall z (φ \to ψ)$
16	3 15	alrimi	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\} \to \forall x \forall y \forall z (φ \to ψ)$
17		ssoprab2	$⊢ \forall x \forall y \forall z (φ \to ψ) \to \{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\}$
18	16 17	impbii	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\} \leftrightarrow \forall x \forall y \forall z (φ \to ψ)$
19	2 1	nfss	$⊢ Ⅎ x \{⟨⟨x, y⟩, z⟩ \| ψ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| φ\}$
20	5 4	nfss	$⊢ Ⅎ y \{⟨⟨x, y⟩, z⟩ \| ψ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| φ\}$
21	8 7	nfss	$⊢ Ⅎ z \{⟨⟨x, y⟩, z⟩ \| ψ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| φ\}$
22		ssel	$⊢ \{⟨⟨x, y⟩, z⟩ \| ψ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| φ\} \to (⟨⟨x, y⟩, z⟩ \in \{⟨⟨x, y⟩, z⟩ \| ψ\} \to ⟨⟨x, y⟩, z⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\})$
23	22 12 11	3imtr3g	$⊢ \{⟨⟨x, y⟩, z⟩ \| ψ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| φ\} \to (ψ \to φ)$
24	21 23	alrimi	$⊢ \{⟨⟨x, y⟩, z⟩ \| ψ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| φ\} \to \forall z (ψ \to φ)$
25	20 24	alrimi	$⊢ \{⟨⟨x, y⟩, z⟩ \| ψ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| φ\} \to \forall y \forall z (ψ \to φ)$
26	19 25	alrimi	$⊢ \{⟨⟨x, y⟩, z⟩ \| ψ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| φ\} \to \forall x \forall y \forall z (ψ \to φ)$
27		ssoprab2	$⊢ \forall x \forall y \forall z (ψ \to φ) \to \{⟨⟨x, y⟩, z⟩ \| ψ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| φ\}$
28	26 27	impbii	$⊢ \{⟨⟨x, y⟩, z⟩ \| ψ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow \forall x \forall y \forall z (ψ \to φ)$
29	18 28	anbi12i	$⊢ (\{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\} \land \{⟨⟨x, y⟩, z⟩ \| ψ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| φ\}) \leftrightarrow (\forall x \forall y \forall z (φ \to ψ) \land \forall x \forall y \forall z (ψ \to φ))$
30		eqss	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨⟨x, y⟩, z⟩ \| ψ\} \leftrightarrow (\{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\} \land \{⟨⟨x, y⟩, z⟩ \| ψ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| φ\})$
31		2albiim	$⊢ \forall y \forall z (φ \leftrightarrow ψ) \leftrightarrow (\forall y \forall z (φ \to ψ) \land \forall y \forall z (ψ \to φ))$
32	31	albii	$⊢ \forall x \forall y \forall z (φ \leftrightarrow ψ) \leftrightarrow \forall x (\forall y \forall z (φ \to ψ) \land \forall y \forall z (ψ \to φ))$
33		19.26	$⊢ \forall x (\forall y \forall z (φ \to ψ) \land \forall y \forall z (ψ \to φ)) \leftrightarrow (\forall x \forall y \forall z (φ \to ψ) \land \forall x \forall y \forall z (ψ \to φ))$
34	32 33	bitri	$⊢ \forall x \forall y \forall z (φ \leftrightarrow ψ) \leftrightarrow (\forall x \forall y \forall z (φ \to ψ) \land \forall x \forall y \forall z (ψ \to φ))$
35	29 30 34	3bitr4i	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨⟨x, y⟩, z⟩ \| ψ\} \leftrightarrow \forall x \forall y \forall z (φ \leftrightarrow ψ)$

Metamath Proof Explorer

Theorem eqoprab2bw

Proof