Metamath Proof Explorer

Theorem dffr2ALT

Description: Alternate proof of dffr2 , which avoids ax-8 but requires ax-10 , ax-11 , ax-12 . (Contributed by NM, 17-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by Mario Carneiro, 23-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dffr2ALT ⊢ R Fr A ↔ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x z ∈ x | z R y = ∅

Proof

Step Hyp Ref Expression
1 df-fr ⊢ R Fr A ↔ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y
2 rabeq0 ⊢ z ∈ x | z R y = ∅ ↔ ∀ z ∈ x ¬ z R y
3 2 rexbii ⊢ ∃ y ∈ x z ∈ x | z R y = ∅ ↔ ∃ y ∈ x ∀ z ∈ x ¬ z R y
4 3 imbi2i ⊢ x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x z ∈ x | z R y = ∅ ↔ x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y
5 4 albii ⊢ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x z ∈ x | z R y = ∅ ↔ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y
6 1 5 bitr4i ⊢ R Fr A ↔ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x z ∈ x | z R y = ∅