Theorem nfcnv 5825

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

Syntax hints:  Ⅎwnfc 2881   class class class wbr 5096  {copab 5158  ^◡ccnv 5621

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 2182  ax-ext 2706

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 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-cnv 5630

This theorem is referenced by:  nfrn  5899  nfpred  6262  nffun  6513  nff1  6726  nfsup  9352  nfinf  9384  gsumcom2  19902  ptbasfi  23523  mbfposr  25607  itg1climres  25669  funcnvmpt  32694  nfwsuc  35959  aomclem8  43245  rfcnpre1  45206  rfcnpre2  45218  smfpimcc  46994