1wlkdlem2

Step	Hyp	Ref	Expression
1		1wlkd.p	$⊢ P = ⟨“ X Y ”⟩$
2		1wlkd.f	$⊢ F = ⟨“ J ”⟩$
3		1wlkd.x	$⊢ φ \to X \in V$
4		1wlkd.y	$⊢ φ \to Y \in V$
5		1wlkd.l	$⊢ (φ \land X = Y) \to I (J) = \{X\}$
6		1wlkd.j	$⊢ (φ \land X \neq Y) \to \{X, Y\} \subseteq I (J)$
7		snidg	$⊢ X \in V \to X \in \{X\}$
8	3 7	syl	$⊢ φ \to X \in \{X\}$
9	8	adantr	$⊢ (φ \land X = Y) \to X \in \{X\}$
10	9 5	eleqtrrd	$⊢ (φ \land X = Y) \to X \in I (J)$
11	4	adantr	$⊢ (φ \land X \neq Y) \to Y \in V$
12		prssg	$⊢ (X \in V \land Y \in V) \to ((X \in I (J) \land Y \in I (J)) \leftrightarrow \{X, Y\} \subseteq I (J))$
13	3 11 12	syl2an2r	$⊢ (φ \land X \neq Y) \to ((X \in I (J) \land Y \in I (J)) \leftrightarrow \{X, Y\} \subseteq I (J))$
14	6 13	mpbird	$⊢ (φ \land X \neq Y) \to (X \in I (J) \land Y \in I (J))$
15	14	simpld	$⊢ (φ \land X \neq Y) \to X \in I (J)$
16	10 15	pm2.61dane	$⊢ φ \to X \in I (J)$

Metamath Proof Explorer