Theorem domeng

Description: Dominance in terms of equinumerosity, with the sethood requirement expressed as an antecedent. Example 1 of Enderton p. 146. (Contributed by NM, 24-Apr-2004)

	Ref	Expression
Assertion	domeng	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 ≼ 𝑦 ↔ 𝐴 ≼ 𝐵 ) )
2		sseq2	⊢ ( 𝑦 = 𝐵 → ( 𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ 𝐵 ) )
3	2	anbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝑦 ) ↔ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) )
4	3	exbidv	⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝑦 ) ↔ ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) )
5		vex	⊢ 𝑦 ∈ V
6	5	domen	⊢ ( 𝐴 ≼ 𝑦 ↔ ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝑦 ) )
7	1 4 6	vtoclbg	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) )