Theorem nfcnv 5751

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.

Step	Hyp	Ref	Expression
1		df-cnv 5565	. 2 ⊢ ◡𝐴 = {⟨𝑦, 𝑧⟩ ∣ 𝑧𝐴𝑦}
2		nfcv 2979	. . . 4 ⊢ Ⅎ𝑥𝑧
3		nfcnv.1	. . . 4 ⊢ Ⅎ𝑥𝐴
4		nfcv 2979	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5115	. . 3 ⊢ Ⅎ𝑥 𝑧𝐴𝑦
6	5	nfopab 5136	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ 𝑧𝐴𝑦}
7	1, 6	nfcxfr 2977	1 ⊢ Ⅎ𝑥◡𝐴

Syntax hints:  Ⅎwnfc 2963   class class class wbr 5068  {copab 5130  ^◡ccnv 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-cnv 5565

This theorem is referenced by:  nfrn  5826  nfpred  6155  nffun  6380  nff1  6575  nfsup  8917  nfinf  8948  gsumcom2  19097  ptbasfi  22191  mbfposr  24255  itg1climres  24317  funcnvmpt  30414  nfwsuc  33107  aomclem8  39668  rfcnpre1  41283  rfcnpre2  41295  smfpimcc  43089