Metamath Proof Explorer

Theorem drnfc2

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Proof revision is marked as discouraged because the minimizer replaces albidv with dral2 , leading to a one byte longer proof. However feel free to manually edit it according to conventions. (TODO: dral2 depends on ax-13 , hence its usage during minimizing is discouraged. Check in the long run whether this is a permanent restriction). Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Mario Carneiro, 8-Oct-2016) Avoid ax-8 . (Revised by Wolf Lammen, 22-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis drnfc1.1 ⊢ ∀ x x = y → A = B
Assertion drnfc2 ⊢ ∀ x x = y → Ⅎ _ z A ↔ Ⅎ _ z B

Proof

Step Hyp Ref Expression
1 drnfc1.1 ⊢ ∀ x x = y → A = B
2 eleq2w2 ⊢ A = B → w ∈ A ↔ w ∈ B
3 1 2 syl ⊢ ∀ x x = y → w ∈ A ↔ w ∈ B
4 3 drnf2 ⊢ ∀ x x = y → Ⅎ z w ∈ A ↔ Ⅎ z w ∈ B
5 4 albidv ⊢ ∀ x x = y → ∀ w Ⅎ z w ∈ A ↔ ∀ w Ⅎ z w ∈ B
6 df-nfc ⊢ Ⅎ _ z A ↔ ∀ w Ⅎ z w ∈ A
7 df-nfc ⊢ Ⅎ _ z B ↔ ∀ w Ⅎ z w ∈ B
8 5 6 7 3bitr4g ⊢ ∀ x x = y → Ⅎ _ z A ↔ Ⅎ _ z B