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	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfcnv	$$⊢\underset{\_}{Ⅎ}x{A}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		nfcnv.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		df-cnv	$$⊢A^{-1}=\left\{⟨y,z⟩|zAy\right\}$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
5	3 1 4	nfbr	$$⊢ℲxzAy$$
6	5	nfopab	$$⊢\underset{\_}{Ⅎ}x\left\{⟨y,z⟩|zAy\right\}$$
7	2 6	nfcxfr	$$⊢\underset{\_}{Ⅎ}x{A}^{-1}$$