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 ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 { 𝑧𝑥𝑧 𝑅 𝑦 } = ∅ ) )

Proof

Step Hyp Ref Expression
1 df-fr ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ) )
2 rabeq0 ( { 𝑧𝑥𝑧 𝑅 𝑦 } = ∅ ↔ ∀ 𝑧𝑥 ¬ 𝑧 𝑅 𝑦 )
3 2 rexbii ( ∃ 𝑦𝑥 { 𝑧𝑥𝑧 𝑅 𝑦 } = ∅ ↔ ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 )
4 3 imbi2i ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 { 𝑧𝑥𝑧 𝑅 𝑦 } = ∅ ) ↔ ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ) )
5 4 albii ( ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 { 𝑧𝑥𝑧 𝑅 𝑦 } = ∅ ) ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ) )
6 1 5 bitr4i ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 { 𝑧𝑥𝑧 𝑅 𝑦 } = ∅ ) )