![]() |
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 2800, 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 2069 | . . 3 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)) | |
2 | df-clab 2706 | . . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
3 | df-clab 2706 | . . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓) | |
4 | 1, 2, 3 | 3bitr4g 314 | . 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∣ 𝜓})) |
5 | 4 | eqrdv 2726 | 1 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1532 = wceq 1534 [wsb 2060 ∈ wcel 2099 {cab 2705 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 |
This theorem is referenced by: abbidv 2797 abbii 2798 abbid 2799 eqab 2868 sbcbi2 3837 iuneq12df 5017 axrep6g 5287 iotabi 6508 uniabio 6509 iotaval 6513 iotanul 6520 iuneq12daf 32340 bj-abv 36378 bj-cleq 36435 abbi1sn 41705 iotain 43848 |
Copyright terms: Public domain | W3C validator |