bnj1309

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	bnj1309.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
	Assertion	bnj1309	$⊢ w \in B \to \forall x w \in B$

Proof

Step	Hyp	Ref	Expression
1		bnj1309.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		hbra1	$⊢ \forall x \in d pred (x, A, R) \subseteq d \to \forall x \forall x \in d pred (x, A, R) \subseteq d$
3	2	bnj1352	$⊢ (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d) \to \forall x (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)$
4	3	hbab	$⊢ w \in \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\} \to \forall x w \in \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
5	1 4	hbxfreq	$⊢ w \in B \to \forall x w \in B$

Metamath Proof Explorer

Theorem bnj1309

Proof