![]() |
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 4874 | . 2 ⊢ 〈𝐴, 𝐵〉 = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) | |
2 | nfop.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfel1 2919 | . . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V |
4 | nfop.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
5 | 4 | nfel1 2919 | . . . 4 ⊢ Ⅎ𝑥 𝐵 ∈ V |
6 | 3, 5 | nfan 1896 | . . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V) |
7 | 2 | nfsn 4711 | . . . 4 ⊢ Ⅎ𝑥{𝐴} |
8 | 2, 4 | nfpr 4696 | . . . 4 ⊢ Ⅎ𝑥{𝐴, 𝐵} |
9 | 7, 8 | nfpr 4696 | . . 3 ⊢ Ⅎ𝑥{{𝐴}, {𝐴, 𝐵}} |
10 | nfcv 2902 | . . 3 ⊢ Ⅎ𝑥∅ | |
11 | 6, 9, 10 | nfif 4560 | . 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) |
12 | 1, 11 | nfcxfr 2900 | 1 ⊢ Ⅎ𝑥〈𝐴, 𝐵〉 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 ∈ wcel 2105 Ⅎwnfc 2887 Vcvv 3477 ∅c0 4338 ifcif 4530 {csn 4630 {cpr 4632 〈cop 4636 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-v 3479 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 |
This theorem is referenced by: nfopd 4894 moop2 5511 iunopeqop 5530 fliftfuns 7333 dfmpo 8125 qliftfuns 8842 xpf1o 9177 nfseq 14048 txcnp 23643 cnmpt1t 23688 cnmpt2t 23696 flfcnp2 24030 nosupbnd2 27775 noinfbnd2 27790 nfseqs 28307 bnj958 34932 bnj1000 34933 bnj1446 35037 bnj1447 35038 bnj1448 35039 bnj1466 35045 bnj1467 35046 bnj1519 35057 bnj1520 35058 bnj1529 35062 poimirlem26 37632 nfopdALT 38952 nfaov 47128 |
Copyright terms: Public domain | W3C validator |