Theorem bj-nfcsym

Description: The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid with additional axioms; see also nfcv ). This could be proved from aecom and nfcvb but the latter requires a domain with at least two objects (hence uses extra axioms). (Contributed by BJ, 30-Sep-2018) Proof modification is discouraged to avoid use of eqcomd instead of equcomd ; removing dependency on ax-ext is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 , eleq2d (using elequ2 ), nfcvf , dvelimc , dvelimdc , nfcvf2 . (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-nfcsym	⊢ ( Ⅎ 𝑥 𝑦 ↔ Ⅎ 𝑦 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		sp	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 )
2	1	equcomd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑦 = 𝑥 )
3	2	drnfc1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( Ⅎ 𝑥 𝑦 ↔ Ⅎ 𝑦 𝑥 ) )
4		nfcvf	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 )
5		nfcvf2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 )
6	4 5	2thd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( Ⅎ 𝑥 𝑦 ↔ Ⅎ 𝑦 𝑥 ) )
7	3 6	pm2.61i	⊢ ( Ⅎ 𝑥 𝑦 ↔ Ⅎ 𝑦 𝑥 )