Metamath Proof Explorer


Theorem zfregfr

Description: The membership relation is well-founded on any class. (Contributed by NM, 26-Nov-1995)

Ref Expression
Assertion zfregfr E Fr 𝐴

Proof

Step Hyp Ref Expression
1 dfepfr ( E Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 ( 𝑥𝑦 ) = ∅ ) )
2 vex 𝑥 ∈ V
3 zfreg ( ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 ( 𝑦𝑥 ) = ∅ )
4 2 3 mpan ( 𝑥 ≠ ∅ → ∃ 𝑦𝑥 ( 𝑦𝑥 ) = ∅ )
5 incom ( 𝑦𝑥 ) = ( 𝑥𝑦 )
6 5 eqeq1i ( ( 𝑦𝑥 ) = ∅ ↔ ( 𝑥𝑦 ) = ∅ )
7 6 rexbii ( ∃ 𝑦𝑥 ( 𝑦𝑥 ) = ∅ ↔ ∃ 𝑦𝑥 ( 𝑥𝑦 ) = ∅ )
8 4 7 sylib ( 𝑥 ≠ ∅ → ∃ 𝑦𝑥 ( 𝑥𝑦 ) = ∅ )
9 8 adantl ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 ( 𝑥𝑦 ) = ∅ )
10 1 9 mpgbir E Fr 𝐴