Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfcnv | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for converse relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Ref | Expression |
---|---|
nfcnv.1 | ⊢ Ⅎ𝑥𝐴 |
Ref | Expression |
---|---|
nfcnv | ⊢ Ⅎ𝑥◡𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-cnv 5597 | . 2 ⊢ ◡𝐴 = {〈𝑦, 𝑧〉 ∣ 𝑧𝐴𝑦} | |
2 | nfcv 2907 | . . . 4 ⊢ Ⅎ𝑥𝑧 | |
3 | nfcnv.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
4 | nfcv 2907 | . . . 4 ⊢ Ⅎ𝑥𝑦 | |
5 | 2, 3, 4 | nfbr 5121 | . . 3 ⊢ Ⅎ𝑥 𝑧𝐴𝑦 |
6 | 5 | nfopab 5143 | . 2 ⊢ Ⅎ𝑥{〈𝑦, 𝑧〉 ∣ 𝑧𝐴𝑦} |
7 | 1, 6 | nfcxfr 2905 | 1 ⊢ Ⅎ𝑥◡𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2887 class class class wbr 5074 {copab 5136 ◡ccnv 5588 |
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-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-br 5075 df-opab 5137 df-cnv 5597 |
This theorem is referenced by: nfrn 5861 nfpred 6207 nffun 6457 nff1 6668 nfsup 9210 nfinf 9241 gsumcom2 19576 ptbasfi 22732 mbfposr 24816 itg1climres 24879 funcnvmpt 31004 nfwsuc 33812 aomclem8 40886 rfcnpre1 42562 rfcnpre2 42574 smfpimcc 44341 |
Copyright terms: Public domain | W3C validator |