Theorem nfcnv

Description: Bound-variable hypothesis builder for converse relation. (Contributed by NM, 31-Jan-2004) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypothesis	nfcnv.1	⊢ Ⅎ 𝑥 𝐴
Assertion	nfcnv	⊢ Ⅎ 𝑥 ◡ 𝐴

Proof

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