Theorem nfcnv 5827

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 5632	. 2 ⊢ ◡𝐴 = {⟨𝑦, 𝑧⟩ ∣ 𝑧𝐴𝑦}
2		nfcv 2898	. . . 4 ⊢ Ⅎ𝑥𝑧
3		nfcnv.1	. . . 4 ⊢ Ⅎ𝑥𝐴
4		nfcv 2898	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5145	. . 3 ⊢ Ⅎ𝑥 𝑧𝐴𝑦
6	5	nfopab 5167	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ 𝑧𝐴𝑦}
7	1, 6	nfcxfr 2896	1 ⊢ Ⅎ𝑥◡𝐴

Syntax hints:  Ⅎwnfc 2883   class class class wbr 5098  {copab 5160  ^◡ccnv 5623

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-cnv 5632

This theorem is referenced by:  nfrn  5901  nfpred  6264  nffun  6515  nff1  6728  nfsup  9354  nfinf  9386  gsumcom2  19904  ptbasfi  23525  mbfposr  25609  itg1climres  25671  funcnvmpt  32745  nfwsuc  36010  aomclem8  43303  rfcnpre1  45264  rfcnpre2  45276  smfpimcc  47052