| 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 |
|---|---|
| dfssf.1 | ⊢ Ⅎ𝑥𝐴 |
| dfssf.2 | ⊢ Ⅎ𝑥𝐵 |
| Ref | Expression |
|---|---|
| nfss | ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfssf.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
| 2 | dfssf.2 | . . 3 ⊢ Ⅎ𝑥𝐵 | |
| 3 | 1, 2 | dfss3f 3975 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) |
| 4 | nfra1 3284 | . 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 | |
| 5 | 3, 4 | nfxfr 1853 | 1 ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: Ⅎwnf 1783 ∈ wcel 2108 Ⅎwnfc 2890 ∀wral 3061 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-10 2141 ax-11 2157 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 df-clel 2816 df-nfc 2892 df-ral 3062 df-ss 3968 |
| This theorem is referenced by: ssrexf 4050 nfpw 4619 ssiun2s 5048 triun 5274 iunopeqop 5526 ssopab2bw 5552 ssopab2b 5554 nffr 5658 nfrel 5789 nffun 6589 nff 6732 fvmptss 7028 ssoprab2b 7502 eqoprab2bw 7503 tfis 7876 ovmptss 8118 nffrecs 8308 nfwrecsOLD 8342 oawordeulem 8592 nnawordex 8675 r1val1 9826 cardaleph 10129 nfsum1 15726 nfsum 15727 nfcprod1 15944 nfcprod 15945 iunconn 23436 ovolfiniun 25536 ovoliunlem3 25539 ovoliun 25540 ovoliun2 25541 ovoliunnul 25542 limciun 25929 ssiun2sf 32572 ssrelf 32627 funimass4f 32647 fsumiunle 32831 prodindf 32848 esumiun 34095 bnj1408 35050 totbndbnd 37796 naddwordnexlem4 43414 ss2iundf 43672 iunconnlem2 44955 iinssdf 45144 rnmptssbi 45267 stoweidlem53 46068 stoweidlem57 46072 meaiunincf 46498 meaiuninc3 46500 opnvonmbllem2 46648 smflim 46792 nfsetrecs 49205 setrec2fun 49211 |
| Copyright terms: Public domain | W3C validator |