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 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ 𝑦 ) = ∅ ) )