Description: Lemma for dfon2 . (Contributed by Scott Fenton, 28-Feb-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | dfon2lem2 | ⊢ ∪ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓 ) } ⊆ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 | ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓 ) → 𝑥 ⊆ 𝐴 ) | |
2 | 1 | ss2abi | ⊢ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓 ) } ⊆ { 𝑥 ∣ 𝑥 ⊆ 𝐴 } |
3 | df-pw | ⊢ 𝒫 𝐴 = { 𝑥 ∣ 𝑥 ⊆ 𝐴 } | |
4 | 2 3 | sseqtrri | ⊢ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓 ) } ⊆ 𝒫 𝐴 |
5 | sspwuni | ⊢ ( { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓 ) } ⊆ 𝒫 𝐴 ↔ ∪ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓 ) } ⊆ 𝐴 ) | |
6 | 4 5 | mpbi | ⊢ ∪ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓 ) } ⊆ 𝐴 |