Metamath Proof Explorer

Theorem friOLD

Description: Obsolete version of fri as of 16-Nov-2024. (Contributed by NM, 18-Mar-1997) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion friOLD ⊢ B ∈ C ∧ R Fr A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x

Proof

Step Hyp Ref Expression
1 df-fr ⊢ R Fr A ↔ ∀ z z ⊆ A ∧ z ≠ ∅ → ∃ x ∈ z ∀ y ∈ z ¬ y R x
2 sseq1 ⊢ z = B → z ⊆ A ↔ B ⊆ A
3 neeq1 ⊢ z = B → z ≠ ∅ ↔ B ≠ ∅
4 2 3 anbi12d ⊢ z = B → z ⊆ A ∧ z ≠ ∅ ↔ B ⊆ A ∧ B ≠ ∅
5 raleq ⊢ z = B → ∀ y ∈ z ¬ y R x ↔ ∀ y ∈ B ¬ y R x
6 5 rexeqbi1dv ⊢ z = B → ∃ x ∈ z ∀ y ∈ z ¬ y R x ↔ ∃ x ∈ B ∀ y ∈ B ¬ y R x
7 4 6 imbi12d ⊢ z = B → z ⊆ A ∧ z ≠ ∅ → ∃ x ∈ z ∀ y ∈ z ¬ y R x ↔ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
8 7 spcgv ⊢ B ∈ C → ∀ z z ⊆ A ∧ z ≠ ∅ → ∃ x ∈ z ∀ y ∈ z ¬ y R x → B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
9 1 8 syl5bi ⊢ B ∈ C → R Fr A → B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
10 9 imp31 ⊢ B ∈ C ∧ R Fr A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x