![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfss | Structured version Visualization version GIF version |
Description: If 𝑥 is not free in 𝐴 and 𝐵, it is not free in 𝐴 ⊆ 𝐵. (Contributed by NM, 27-Dec-1996.) |
Ref | Expression |
---|---|
dfss2f.1 | ⊢ Ⅎ𝑥𝐴 |
dfss2f.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfss | ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfss2f.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
2 | dfss2f.2 | . . 3 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | dfss3f 3812 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) |
4 | nfra1 3122 | . 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 | |
5 | 3, 4 | nfxfr 1897 | 1 ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1827 ∈ wcel 2106 Ⅎwnfc 2918 ∀wral 3089 ⊆ wss 3791 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-ext 2753 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-ral 3094 df-in 3798 df-ss 3805 |
This theorem is referenced by: ssrexf 3883 nfpw 4392 ssiun2s 4797 triun 5000 iunopeqop 5218 ssopab2b 5239 nffr 5329 nfrel 5452 nffun 6158 nff 6287 fvmptss 6553 ssoprab2b 6989 tfis 7332 ovmptss 7539 nfwrecs 7691 oawordeulem 7918 nnawordex 8001 r1val1 8946 cardaleph 9245 nfsum1 14828 nfsum 14829 nfcprod1 15043 nfcprod 15044 iunconn 21640 ovolfiniun 23705 ovoliunlem3 23708 ovoliun 23709 ovoliun2 23710 ovoliunnul 23711 limciun 24095 ssiun2sf 29940 ssrelf 29990 funimass4f 30002 fsumiunle 30139 prodindf 30683 esumiun 30754 bnj1408 31703 nffrecs 32367 totbndbnd 34196 ss2iundf 38890 iunconnlem2 40086 iinssdf 40236 rnmptssbi 40370 stoweidlem53 41179 stoweidlem57 41183 meaiunincf 41606 meaiuninc3 41608 opnvonmbllem2 41756 smflim 41894 nfsetrecs 43520 setrec2fun 43526 |
Copyright terms: Public domain | W3C validator |