| 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 4870 | . 2 ⊢ 〈𝐴, 𝐵〉 = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) | |
| 2 | nfop.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
| 3 | 2 | nfel1 2922 | . . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V |
| 4 | nfop.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
| 5 | 4 | nfel1 2922 | . . . 4 ⊢ Ⅎ𝑥 𝐵 ∈ V |
| 6 | 3, 5 | nfan 1899 | . . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V) |
| 7 | 2 | nfsn 4707 | . . . 4 ⊢ Ⅎ𝑥{𝐴} |
| 8 | 2, 4 | nfpr 4692 | . . . 4 ⊢ Ⅎ𝑥{𝐴, 𝐵} |
| 9 | 7, 8 | nfpr 4692 | . . 3 ⊢ Ⅎ𝑥{{𝐴}, {𝐴, 𝐵}} |
| 10 | nfcv 2905 | . . 3 ⊢ Ⅎ𝑥∅ | |
| 11 | 6, 9, 10 | nfif 4556 | . 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) |
| 12 | 1, 11 | nfcxfr 2903 | 1 ⊢ Ⅎ𝑥〈𝐴, 𝐵〉 |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 ∈ wcel 2108 Ⅎwnfc 2890 Vcvv 3480 ∅c0 4333 ifcif 4525 {csn 4626 {cpr 4628 〈cop 4632 |
| 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-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 |
| This theorem is referenced by: nfopd 4890 moop2 5507 iunopeqop 5526 fliftfuns 7334 dfmpo 8127 qliftfuns 8844 xpf1o 9179 nfseq 14052 txcnp 23628 cnmpt1t 23673 cnmpt2t 23681 flfcnp2 24015 nosupbnd2 27761 noinfbnd2 27776 nfseqs 28293 bnj958 34954 bnj1000 34955 bnj1446 35059 bnj1447 35060 bnj1448 35061 bnj1466 35067 bnj1467 35068 bnj1519 35079 bnj1520 35080 bnj1529 35084 poimirlem26 37653 nfopdALT 38972 nfaov 47191 |
| Copyright terms: Public domain | W3C validator |