Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > opabbii | Structured version Visualization version GIF version |
Description: Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
Ref | Expression |
---|---|
opabbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
opabbii | ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2819 | . 2 ⊢ 𝑧 = 𝑧 | |
2 | opabbii.1 | . . . 4 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | a1i 11 | . . 3 ⊢ (𝑧 = 𝑧 → (𝜑 ↔ 𝜓)) |
4 | 3 | opabbidv 5123 | . 2 ⊢ (𝑧 = 𝑧 → {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓}) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 = wceq 1531 {copab 5119 |
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 1905 ax-6 1964 ax-7 2009 ax-9 2118 ax-12 2170 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-opab 5120 |
This theorem is referenced by: mptv 5162 2rbropap 5442 dfid4 5454 fconstmpt 5607 xpundi 5613 xpundir 5614 inxp 5696 csbcnv 5747 cnvco 5749 resopab 5895 opabresid 5910 opabresidOLD 5912 cnvi 5993 cnvun 5994 cnvxp 6007 cnvcnv3 6038 coundi 6093 coundir 6094 mptun 6487 fvopab6 6794 fmptsng 6923 fmptsnd 6924 cbvoprab1 7233 cbvoprab12 7235 dmoprabss 7248 mpomptx 7257 resoprab 7262 elrnmpores 7280 ov6g 7304 1st2val 7709 2nd2val 7710 dfoprab3s 7743 dfoprab3 7744 dfoprab4 7745 opabn1stprc 7748 mptmpoopabbrd 7770 fsplit 7804 fsplitOLD 7805 mapsncnv 8449 xpcomco 8599 marypha2lem2 8892 oemapso 9137 leweon 9429 r0weon 9430 compsscnv 9785 fpwwe 10060 ltrelxr 10694 ltxrlt 10703 ltxr 12502 shftidt2 14432 prdsle 16727 prdsless 16728 prdsleval 16742 dfiso2 17034 joindm 17605 meetdm 17619 gaorb 18429 efgcpbllema 18872 frgpuplem 18890 ltbval 20244 ltbwe 20245 opsrle 20248 opsrtoslem1 20256 opsrtoslem2 20257 dvdsrzring 20622 pjfval2 20845 lmfval 21832 lmbr 21858 lgsquadlem3 25950 perpln1 26488 outpasch 26533 ishpg 26537 axcontlem2 26743 wksfval 27383 wlkson 27430 pthsfval 27494 ispth 27496 dfadj2 29654 dmadjss 29656 cnvadj 29661 mpomptxf 30417 satfv0 32598 satfvsuclem1 32599 satfvsuclem2 32600 satfbrsuc 32606 satf0 32612 satf0suclem 32615 fmlasuc0 32624 fneer 33694 bj-dfmpoa 34402 bj-mpomptALT 34403 bj-brab2a1 34433 opropabco 34991 cnvepres 35547 inxp2 35611 xrninxp 35632 xrninxp2 35633 rnxrnres 35639 rnxrncnvepres 35640 rnxrnidres 35641 dfcoss2 35653 dfcoss3 35654 1cossres 35666 dfcoels 35667 br1cosscnvxrn 35706 1cosscnvxrn 35707 coss0 35711 cossid 35712 dfssr2 35731 cmtfvalN 36338 cmtvalN 36339 cvrfval 36396 cvrval 36397 dicval2 38307 fgraphopab 39801 fgraphxp 39802 mptssid 41501 dfnelbr2 43463 opabbrfex0d 43476 opabbrfexd 43478 upwlksfval 44001 xpsnopab 44023 mpomptx2 44374 |
Copyright terms: Public domain | W3C validator |