![]() |
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 3974 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) |
4 | nfra1 3282 | . 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 | |
5 | 3, 4 | nfxfr 1856 | 1 ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1786 ∈ wcel 2107 Ⅎwnfc 2884 ∀wral 3062 ⊆ wss 3949 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-v 3477 df-in 3956 df-ss 3966 |
This theorem is referenced by: ssrexf 4049 nfpw 4622 ssiun2s 5052 triun 5281 iunopeqop 5522 ssopab2bw 5548 ssopab2b 5550 nffr 5651 nfrel 5780 nffun 6572 nff 6714 fvmptss 7011 ssoprab2b 7478 eqoprab2bw 7479 tfis 7844 ovmptss 8079 nffrecs 8268 nfwrecsOLD 8302 oawordeulem 8554 nnawordex 8637 r1val1 9781 cardaleph 10084 nfsum1 15636 nfsum 15637 nfcprod1 15854 nfcprod 15855 iunconn 22932 ovolfiniun 25018 ovoliunlem3 25021 ovoliun 25022 ovoliun2 25023 ovoliunnul 25024 limciun 25411 ssiun2sf 31791 ssrelf 31844 funimass4f 31861 fsumiunle 32035 prodindf 33021 esumiun 33092 bnj1408 34047 totbndbnd 36657 naddwordnexlem4 42152 ss2iundf 42410 iunconnlem2 43696 iinssdf 43828 rnmptssbi 43965 stoweidlem53 44769 stoweidlem57 44773 meaiunincf 45199 meaiuninc3 45201 opnvonmbllem2 45349 smflim 45493 nfsetrecs 47731 setrec2fun 47737 |
Copyright terms: Public domain | W3C validator |