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

Theorem nfcnv 5832
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 5639 . 2 𝐴 = {⟨𝑦, 𝑧⟩ ∣ 𝑧𝐴𝑦}
2 nfcv 2905 . . . 4 𝑥𝑧
3 nfcnv.1 . . . 4 𝑥𝐴
4 nfcv 2905 . . . 4 𝑥𝑦
52, 3, 4nfbr 5150 . . 3 𝑥 𝑧𝐴𝑦
65nfopab 5172 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ 𝑧𝐴𝑦}
71, 6nfcxfr 2903 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:  wnfc 2885   class class class wbr 5103  {copab 5165  ccnv 5630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5166  df-cnv 5639
This theorem is referenced by:  nfrn  5905  nfpred  6256  nffun  6521  nff1  6733  nfsup  9383  nfinf  9414  gsumcom2  19743  ptbasfi  22916  mbfposr  25000  itg1climres  25063  funcnvmpt  31469  nfwsuc  34263  aomclem8  41326  rfcnpre1  43166  rfcnpre2  43178  smfpimcc  44981
  Copyright terms: Public domain W3C validator