MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfcnv Structured version   Visualization version   GIF version

Theorem nfcnv 5787
Description: Bound-variable hypothesis builder for converse relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
Hypothesis
Ref Expression
nfcnv.1 𝑥𝐴
Assertion
Ref Expression
nfcnv 𝑥𝐴

Proof of Theorem nfcnv
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-cnv 5597 . 2 𝐴 = {⟨𝑦, 𝑧⟩ ∣ 𝑧𝐴𝑦}
2 nfcv 2907 . . . 4 𝑥𝑧
3 nfcnv.1 . . . 4 𝑥𝐴
4 nfcv 2907 . . . 4 𝑥𝑦
52, 3, 4nfbr 5121 . . 3 𝑥 𝑧𝐴𝑦
65nfopab 5143 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ 𝑧𝐴𝑦}
71, 6nfcxfr 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