Theorem nfcnv 5828

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

Syntax hints:  Ⅎwnfc 2884   class class class wbr 5086  {copab 5148  ^◡ccnv 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-cnv 5633

This theorem is referenced by:  nfrn  5902  nfpred  6265  nffun  6516  nff1  6729  funcnvmpt  6944  nfsup  9358  nfinf  9390  gsumcom2  19944  ptbasfi  23559  mbfposr  25632  itg1climres  25694  nfwsuc  36017  aomclem8  43510  rfcnpre1  45471  rfcnpre2  45483  smfpimcc  47257