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

Theorem nfcnv 5748
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 5562 . 2 𝐴 = {⟨𝑦, 𝑧⟩ ∣ 𝑧𝐴𝑦}
2 nfcv 2982 . . . 4 𝑥𝑧
3 nfcnv.1 . . . 4 𝑥𝐴
4 nfcv 2982 . . . 4 𝑥𝑦
52, 3, 4nfbr 5110 . . 3 𝑥 𝑧𝐴𝑦
65nfopab 5131 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ 𝑧𝐴𝑦}
71, 6nfcxfr 2980 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:  wnfc 2966   class class class wbr 5063  {copab 5125  ccnv 5553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064  df-opab 5126  df-cnv 5562
This theorem is referenced by:  nfrn  5823  nfpred  6152  nffun  6377  nff1  6572  nfsup  8909  nfinf  8940  gsumcom2  19031  ptbasfi  22124  mbfposr  24187  itg1climres  24249  funcnvmpt  30346  nfwsuc  33008  aomclem8  39545  rfcnpre1  41160  rfcnpre2  41172  smfpimcc  42967
  Copyright terms: Public domain W3C validator