Theorem epfrc

Description: A subset of a well-founded class has a minimal element. (Contributed by NM, 17-Feb-2004) (Revised by David Abernethy, 22-Feb-2011)

	Ref	Expression
Hypothesis	epfrc.1	⊢ 𝐵 ∈ V
Assertion	epfrc	⊢ ( ( E Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ( 𝐵 ∩ 𝑥 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		epfrc.1	⊢ 𝐵 ∈ V
2	1	frc	⊢ ( ( E Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 { 𝑦 ∈ 𝐵 ∣ 𝑦 E 𝑥 } = ∅ )
3		dfin5	⊢ ( 𝐵 ∩ 𝑥 ) = { 𝑦 ∈ 𝐵 ∣ 𝑦 ∈ 𝑥 }
4		epel	⊢ ( 𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥 )
5	4	rabbii	⊢ { 𝑦 ∈ 𝐵 ∣ 𝑦 E 𝑥 } = { 𝑦 ∈ 𝐵 ∣ 𝑦 ∈ 𝑥 }
6	3 5	eqtr4i	⊢ ( 𝐵 ∩ 𝑥 ) = { 𝑦 ∈ 𝐵 ∣ 𝑦 E 𝑥 }
7	6	eqeq1i	⊢ ( ( 𝐵 ∩ 𝑥 ) = ∅ ↔ { 𝑦 ∈ 𝐵 ∣ 𝑦 E 𝑥 } = ∅ )
8	7	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝐵 ∩ 𝑥 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐵 { 𝑦 ∈ 𝐵 ∣ 𝑦 E 𝑥 } = ∅ )
9	2 8	sylibr	⊢ ( ( E Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ( 𝐵 ∩ 𝑥 ) = ∅ )