|   | 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 3973 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | 
| 4 | df-ral 3061 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
| 5 | 3, 4 | bitr4i 278 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1537 ∈ wcel 2107 Ⅎwnfc 2889 ∀wral 3060 ⊆ wss 3950 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-11 2156 ax-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-nf 1783 df-clel 2815 df-nfc 2891 df-ral 3061 df-ss 3967 | 
| This theorem is referenced by: nfss 3975 sigaclcu2 34122 bnj1498 35076 heibor1 37818 ssrabf 45124 ssrab2f 45127 limsupequzmpt2 45738 liminfequzmpt2 45811 pimconstlt1 46722 pimltpnff 46723 pimiooltgt 46730 pimdecfgtioc 46735 pimincfltioc 46736 pimdecfgtioo 46737 pimincfltioo 46738 pimgtmnff 46742 sssmf 46758 | 
| Copyright terms: Public domain | W3C validator |