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

Theorem nfcnv 5721
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 5533 . 2 𝐴 = {⟨𝑦, 𝑧⟩ ∣ 𝑧𝐴𝑦}
2 nfcv 2899 . . . 4 𝑥𝑧
3 nfcnv.1 . . . 4 𝑥𝐴
4 nfcv 2899 . . . 4 𝑥𝑦
52, 3, 4nfbr 5077 . . 3 𝑥 𝑧𝐴𝑦
65nfopab 5098 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ 𝑧𝐴𝑦}
71, 6nfcxfr 2897 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:  wnfc 2879   class class class wbr 5030  {copab 5092  ccnv 5524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-v 3400  df-dif 3846  df-un 3848  df-nul 4212  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-br 5031  df-opab 5093  df-cnv 5533
This theorem is referenced by:  nfrn  5795  nfpred  6134  nffun  6362  nff1  6572  nfsup  8990  nfinf  9021  gsumcom2  19216  ptbasfi  22334  mbfposr  24406  itg1climres  24469  funcnvmpt  30581  nfwsuc  33427  aomclem8  40480  rfcnpre1  42122  rfcnpre2  42134  smfpimcc  43902
  Copyright terms: Public domain W3C validator