![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > abbi | Structured version Visualization version GIF version |
Description: Equivalent formulas yield equal class abstractions (closed form). This is the backward implication of abbib 2809, proved from fewer axioms, and hence is independently named. (Contributed by BJ and WL and SN, 20-Aug-2023.) |
Ref | Expression |
---|---|
abbi | ⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spsbbi 2071 | . . 3 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)) | |
2 | df-clab 2713 | . . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
3 | df-clab 2713 | . . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓) | |
4 | 1, 2, 3 | 3bitr4g 314 | . 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∣ 𝜓})) |
5 | 4 | eqrdv 2733 | 1 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∀wal 1535 = wceq 1537 [wsb 2062 ∈ wcel 2106 {cab 2712 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 |
This theorem is referenced by: abbidv 2806 abbii 2807 abbid 2808 eqab 2878 sbcbi2 3854 iuneq12df 5023 axrep6g 5296 iotabi 6529 uniabio 6530 iotaval 6534 iotanul 6541 iuneq12daf 32577 bj-abv 36889 bj-cleq 36945 abbi1sn 42241 iotain 44413 |
Copyright terms: Public domain | W3C validator |