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 3560 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) |
4 | nfra1 2925 | . 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 | |
5 | 3, 4 | nfxfr 1771 | 1 ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1699 ∈ wcel 1977 Ⅎwnfc 2738 ∀wral 2896 ⊆ wss 3540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-in 3547 df-ss 3554 |
This theorem is referenced by: ssrexf 3628 nfpw 4120 ssiun2s 4500 triun 4694 iunopeqop 4906 ssopab2b 4927 nffr 5012 nfrel 5127 nffun 5826 nff 5954 fvmptss 6201 ssoprab2b 6610 tfis 6946 ovmptss 7145 nfwrecs 7296 oawordeulem 7521 nnawordex 7604 r1val1 8532 cardaleph 8795 nfsum1 14268 nfsum 14269 nfcprod1 14479 nfcprod 14480 iuncon 21041 ovolfiniun 23076 ovoliunlem3 23079 ovoliun 23080 ovoliun2 23081 ovoliunnul 23082 limciun 23464 ssiun2sf 28760 ssrelf 28805 funimass4f 28818 esumiun 29483 bnj1408 30358 totbndbnd 32758 ss2iundf 36970 iunconlem2 38193 stoweidlem53 38946 stoweidlem57 38950 opnvonmbllem2 39523 smflim 39663 nfsetrecs 42232 setrec2fun 42238 |
Copyright terms: Public domain | W3C validator |