| 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 2811, 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 2073 | . . 3 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)) | |
| 2 | df-clab 2715 | . . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
| 3 | df-clab 2715 | . . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓) | |
| 4 | 1, 2, 3 | 3bitr4g 314 | . 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∣ 𝜓})) |
| 5 | 4 | eqrdv 2735 | 1 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 = wceq 1540 [wsb 2064 ∈ wcel 2108 {cab 2714 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 |
| This theorem is referenced by: abbidv 2808 abbii 2809 abbid 2810 eqab 2880 sbcbi2 3848 iuneq12df 5018 axrep6g 5290 iotabi 6527 uniabio 6528 iotaval 6532 iotanul 6539 iuneq12daf 32569 bj-abv 36907 bj-cleq 36963 abbi1sn 42262 iotain 44436 |
| Copyright terms: Public domain | W3C validator |