![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfss3f | Structured version Visualization version GIF version |
Description: Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.) |
Ref | Expression |
---|---|
dfssf.1 | ⊢ Ⅎ𝑥𝐴 |
dfssf.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
dfss3f | ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfssf.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
2 | dfssf.2 | . . 3 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | dfssf 3986 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
4 | df-ral 3060 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
5 | 3, 4 | bitr4i 278 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∀wal 1535 ∈ wcel 2106 Ⅎwnfc 2888 ∀wral 3059 ⊆ wss 3963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-11 2155 ax-12 2175 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-nf 1781 df-clel 2814 df-nfc 2890 df-ral 3060 df-ss 3980 |
This theorem is referenced by: nfss 3988 sigaclcu2 34101 bnj1498 35054 heibor1 37797 ssrabf 45054 ssrab2f 45057 limsupequzmpt2 45674 liminfequzmpt2 45747 pimconstlt1 46658 pimltpnff 46659 pimiooltgt 46666 pimdecfgtioc 46671 pimincfltioc 46672 pimdecfgtioo 46673 pimincfltioo 46674 pimgtmnff 46678 sssmf 46694 |
Copyright terms: Public domain | W3C validator |