Metamath Proof Explorer


Theorem dfepfr

Description: An alternate way of saying that the membership relation is well-founded. (Contributed by NM, 17-Feb-2004) (Revised by Mario Carneiro, 23-Jun-2015)

Ref Expression
Assertion dfepfr ( E Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 ( 𝑥𝑦 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 dffr2 ( E Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 { 𝑧𝑥𝑧 E 𝑦 } = ∅ ) )
2 epel ( 𝑧 E 𝑦𝑧𝑦 )
3 2 rabbii { 𝑧𝑥𝑧 E 𝑦 } = { 𝑧𝑥𝑧𝑦 }
4 dfin5 ( 𝑥𝑦 ) = { 𝑧𝑥𝑧𝑦 }
5 3 4 eqtr4i { 𝑧𝑥𝑧 E 𝑦 } = ( 𝑥𝑦 )
6 5 eqeq1i ( { 𝑧𝑥𝑧 E 𝑦 } = ∅ ↔ ( 𝑥𝑦 ) = ∅ )
7 6 rexbii ( ∃ 𝑦𝑥 { 𝑧𝑥𝑧 E 𝑦 } = ∅ ↔ ∃ 𝑦𝑥 ( 𝑥𝑦 ) = ∅ )
8 7 imbi2i ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 { 𝑧𝑥𝑧 E 𝑦 } = ∅ ) ↔ ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 ( 𝑥𝑦 ) = ∅ ) )
9 8 albii ( ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 { 𝑧𝑥𝑧 E 𝑦 } = ∅ ) ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 ( 𝑥𝑦 ) = ∅ ) )
10 1 9 bitri ( E Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 ( 𝑥𝑦 ) = ∅ ) )