Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfop | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.) |
Ref | Expression |
---|---|
nfop.1 | ⊢ Ⅎ𝑥𝐴 |
nfop.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfop | ⊢ Ⅎ𝑥〈𝐴, 𝐵〉 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfopif 4800 | . 2 ⊢ 〈𝐴, 𝐵〉 = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) | |
2 | nfop.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfel1 2923 | . . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V |
4 | nfop.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
5 | 4 | nfel1 2923 | . . . 4 ⊢ Ⅎ𝑥 𝐵 ∈ V |
6 | 3, 5 | nfan 1902 | . . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V) |
7 | 2 | nfsn 4643 | . . . 4 ⊢ Ⅎ𝑥{𝐴} |
8 | 2, 4 | nfpr 4626 | . . . 4 ⊢ Ⅎ𝑥{𝐴, 𝐵} |
9 | 7, 8 | nfpr 4626 | . . 3 ⊢ Ⅎ𝑥{{𝐴}, {𝐴, 𝐵}} |
10 | nfcv 2907 | . . 3 ⊢ Ⅎ𝑥∅ | |
11 | 6, 9, 10 | nfif 4489 | . 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) |
12 | 1, 11 | nfcxfr 2905 | 1 ⊢ Ⅎ𝑥〈𝐴, 𝐵〉 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 ∈ wcel 2106 Ⅎwnfc 2887 Vcvv 3432 ∅c0 4256 ifcif 4459 {csn 4561 {cpr 4563 〈cop 4567 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-v 3434 df-dif 3890 df-un 3892 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 |
This theorem is referenced by: nfopd 4821 moop2 5416 iunopeqop 5435 fliftfuns 7185 dfmpo 7942 qliftfuns 8593 xpf1o 8926 nfseq 13731 txcnp 22771 cnmpt1t 22816 cnmpt2t 22824 flfcnp2 23158 bnj958 32920 bnj1000 32921 bnj1446 33025 bnj1447 33026 bnj1448 33027 bnj1466 33033 bnj1467 33034 bnj1519 33045 bnj1520 33046 bnj1529 33050 nosupbnd2 33919 noinfbnd2 33934 poimirlem26 35803 nfopdALT 36985 nfaov 44671 |
Copyright terms: Public domain | W3C validator |