Theorem nfcnv 5863

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 5667	. 2 ⊢ ◡𝐴 = {⟨𝑦, 𝑧⟩ ∣ 𝑧𝐴𝑦}
2		nfcv 2899	. . . 4 ⊢ Ⅎ𝑥𝑧
3		nfcnv.1	. . . 4 ⊢ Ⅎ𝑥𝐴
4		nfcv 2899	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5171	. . 3 ⊢ Ⅎ𝑥 𝑧𝐴𝑦
6	5	nfopab 5193	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ 𝑧𝐴𝑦}
7	1, 6	nfcxfr 2897	1 ⊢ Ⅎ𝑥◡𝐴

Syntax hints:  Ⅎwnfc 2884   class class class wbr 5124  {copab 5186  ^◡ccnv 5658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-cnv 5667

This theorem is referenced by:  nfrn  5937  nfpred  6300  nffun  6564  nff1  6777  nfsup  9468  nfinf  9500  gsumcom2  19961  ptbasfi  23524  mbfposr  25610  itg1climres  25672  funcnvmpt  32650  nfwsuc  35841  aomclem8  43052  rfcnpre1  45010  rfcnpre2  45022  smfpimcc  46804