| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > eqabi | Structured version Visualization version GIF version | ||
| Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2157. (Revised by Wolf Lammen, 6-May-2023.) |
| Ref | Expression |
|---|---|
| eqabi.1 | ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) |
| Ref | Expression |
|---|---|
| eqabi | ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqabi.1 | . . . 4 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) | |
| 2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑)) |
| 3 | 2 | eqabdv 2875 | . 2 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑}) |
| 4 | 3 | mptru 1547 | 1 ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 = wceq 1540 ⊤wtru 1541 ∈ 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-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 |
| This theorem is referenced by: abid1 2878 cbvralcsf 3941 cbvreucsf 3943 cbvrabcsf 3944 dfsymdif4 4259 dfsymdif2 4261 dfpr2 4646 dftp2 4691 iunid 5060 0iin 5064 pwpwab 5103 epse 5667 pwvabrel 5736 fv3 6924 fo1st 8034 fo2nd 8035 xp2 8051 tfrlem3 8418 ixpconstg 8946 ixp0x 8966 ruv 9642 dfom4 9689 cardnum 10134 alephiso 10138 nnzrab 12645 nn0zrab 12646 qnnen 16249 bdayfo 27722 madeval2 27892 h2hcau 30998 dfch2 31426 hhcno 31923 hhcnf 31924 pjhmopidm 32202 fobigcup 35901 dfsingles2 35922 dfrecs2 35951 dfrdg4 35952 dfint3 35953 bj-snglinv 36973 ecres 38279 dfdm6 38302 ruvALT 42679 rp-abid 43391 dfuniv2 44321 compeq 44459 dfnrm2 48829 dfnrm3 48830 dftermc2 49150 |
| Copyright terms: Public domain | W3C validator |