Theorem bj-ceqsalt

Description: Remove from ceqsalt dependency on ax-ext (and on df-cleq and df-v ). Note: this is not doable with ceqsralt (or ceqsralv ), which uses eleq1 , but the same dependence removal is possible for ceqsalg , ceqsal , ceqsalv , cgsexg , cgsex2g , cgsex4g , ceqsex , ceqsexv , ceqsex2 , ceqsex2v , ceqsex3v , ceqsex4v , ceqsex6v , ceqsex8v , gencbvex (after changing A = y to y = A ), gencbvex2 , gencbval , vtoclgft (it uses F/_ , whose justification nfcjust does not use ax-ext ) and several other vtocl* theorems (see for instance bj-vtoclg1f ). See also bj-ceqsaltv . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-ceqsalt	⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		elisset	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 )
2	1	3anim3i	⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝑉 ) → ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ∃ 𝑥 𝑥 = 𝐴 ) )
3		bj-ceqsalt0	⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ∃ 𝑥 𝑥 = 𝐴 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) )
4	2 3	syl	⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) )