![]() |
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 3968 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) |
4 | nfra1 3271 | . 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 | |
5 | 3, 4 | nfxfr 1847 | 1 ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1777 ∈ wcel 2098 Ⅎwnfc 2875 ∀wral 3050 ⊆ wss 3944 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-10 2129 ax-11 2146 ax-12 2166 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-ex 1774 df-nf 1778 df-clel 2802 df-nfc 2877 df-ral 3051 df-ss 3961 |
This theorem is referenced by: ssrexf 4043 nfpw 4623 ssiun2s 5052 triun 5281 iunopeqop 5523 ssopab2bw 5549 ssopab2b 5551 nffr 5652 nfrel 5781 nffun 6577 nff 6719 fvmptss 7016 ssoprab2b 7489 eqoprab2bw 7490 tfis 7860 ovmptss 8098 nffrecs 8289 nfwrecsOLD 8323 oawordeulem 8575 nnawordex 8658 r1val1 9811 cardaleph 10114 nfsum1 15672 nfsum 15673 nfcprod1 15890 nfcprod 15891 iunconn 23376 ovolfiniun 25474 ovoliunlem3 25477 ovoliun 25478 ovoliun2 25479 ovoliunnul 25480 limciun 25867 ssiun2sf 32429 ssrelf 32484 funimass4f 32503 fsumiunle 32677 prodindf 33773 esumiun 33844 bnj1408 34798 totbndbnd 37393 naddwordnexlem4 42973 ss2iundf 43231 iunconnlem2 44516 iinssdf 44645 rnmptssbi 44775 stoweidlem53 45579 stoweidlem57 45583 meaiunincf 46009 meaiuninc3 46011 opnvonmbllem2 46159 smflim 46303 nfsetrecs 48303 setrec2fun 48309 |
Copyright terms: Public domain | W3C validator |