Metamath Proof Explorer

Theorem drnfc2OLD

Description: Obsolete version of drnfc2 as of 22-Sep-2024. (Contributed by Mario Carneiro, 8-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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